The point is that LLMs and similar tools tend to be very good at automating the trifle but not very useful at what would be considered really "interesting" work

The point is that LLMs and similar tools tend to be very good at automating the trifle but not very useful at what would be considered really "interesting" work. So while your point is somewhat true [0], as he mentions that these tools could become good enough to do the formal verification part, it's precisely not the interesting part. See [1] and [2]; in particular some things that are very easy to do in real maths can be very challenging in an automated theorem prover, quoting from [2]: >In the analyst's dialect of Mathematical English, this is a one-line proof, namely "by the standard limiting argument". Unpacking this into a formal proof required me to go through a fair bit of the Mathlib documentation [...] It's impressive to be able to do such mathematics in Lean/Coq..; at all, but it is very tedious mechanical work [3]. >It was more tedious than I expected, with each line of proof taking about an hour to formalize So I think that rather proves the point of what LLMs are currently good for, and what tools can help for really difficult tasks, rather than invalidate it. [0] https://mathstodon.xyz/@tao/111305365372766606 https://mathstodon.xyz/@tao/111305365372766606 [1] https://mathstodon.xyz/@tao/111305336701455719 https://mathstodon.xyz/@tao/111305336701455719 [2] https://mathstodon.xyz/@tao/111259986983504485 https://mathstodon.xyz/@tao/111259986983504485 [3] https://mathstodon.xyz/@tao/111305336701455719 https://mathstodon.xyz/@tao/111305336701455719