> Math is, of course, an ideal field for AI to work in.
I find it interesting that you state this as obvious. When ChatGPT was introduced four years ago, the argument was that language was fuzzy and probabilistic and that LLMs would thereby never work in math.
It's not hard to tie a deterministic process to any stream of output. The thing "hand waves" a proof and some other process exhaustively searches for either lean operations or some other math-manipulator operations that may create a real proof. The processes go back and forth. A proof is a verifiable string at the end of the day and this is better-than-pure-brute-strategy search strategy guided by heuristics from math literature.
I think someone asked here a bit ago whether other search strategies using OpenAI levels of compute have been tried and think the answer is no (even 3 hours of present GPU computer I think is vast compared to anything available 10 years ago, say).
I find it interesting that you state this as obvious. When ChatGPT was introduced four years ago, the argument was that language was fuzzy and probabilistic and that LLMs would thereby never work in math.