LLMs could be very useful in formalizing the problem and assumptions (conversion from natural language), but once problem is described in a formal way (it can be described in some fuzzy logic), then more reliable AI techniques should be applied.
Interestingly, Tao mentions https://teorth.github.io/equational_theories/, and I believe this is better progress than LLMs doing math. I believe enhancing Lean with more tactics and formalizing those in Lean itself is a more fruitful avenue for AI in math.
I used to work quite extensively with Isabelle and as a developer on Sledgehammer [1]. There are well-known results, most obviously the halting problem, that mean fully-automated logical methods applied to a formalism with any expressive capability, i.e. that can be used to formalize non-trivial problems, simply can never fulfill the role you seem to be suggesting. The proofs that are actually generated in that way are, anyway, horrendous -- in fact, the problem I used to work on was using graph algorithms to try and simplify computer-generated proofs for human comprehension. That's the very reason that all the serious work has previously been on proof /assistants/ and formal validation.
LLMs, especially in /conjunction/ with Lean for formal validation, are really an exciting new frontier in mathematics and it's a mistake to see that as just "unreliable" versus "reliable" symbolic AI etc. The OP Terence Tao has been pushing the edge here since day one and providing, I think, the most unbiased perspective on where things stand today, strengths as much as limitations.
LLMs (as well as humans) are algorithms like anything else and so they are also subject to halting problem. I don't see what LLMs do that couldn't be in principle formalized as a Lean tactic. (IMHO LLMs are just learning rules - theorems of some kind of fuzzy logic - and then try to apply them using heuristic search to satisfy the goal. Unfortunately the rules learned are likely not fully consistent and so you get reasoning errors.)
Comments
LLMs could be very useful in formalizing the problem and assumptions (conversion from natural language), but once problem is described in a formal way (it can be described in some fuzzy logic), then more reliable AI techniques should be applied.
Interestingly, Tao mentions https://teorth.github.io/equational_theories/, and I believe this is better progress than LLMs doing math. I believe enhancing Lean with more tactics and formalizing those in Lean itself is a more fruitful avenue for AI in math.
I used to work quite extensively with Isabelle and as a developer on Sledgehammer [1]. There are well-known results, most obviously the halting problem, that mean fully-automated logical methods applied to a formalism with any expressive capability, i.e. that can be used to formalize non-trivial problems, simply can never fulfill the role you seem to be suggesting. The proofs that are actually generated in that way are, anyway, horrendous -- in fact, the problem I used to work on was using graph algorithms to try and simplify computer-generated proofs for human comprehension. That's the very reason that all the serious work has previously been on proof /assistants/ and formal validation.
LLMs, especially in /conjunction/ with Lean for formal validation, are really an exciting new frontier in mathematics and it's a mistake to see that as just "unreliable" versus "reliable" symbolic AI etc. The OP Terence Tao has been pushing the edge here since day one and providing, I think, the most unbiased perspective on where things stand today, strengths as much as limitations.
[1] https://isabelle.in.tum.de/website-Isabelle2009-1/sledgehamm...
LLMs (as well as humans) are algorithms like anything else and so they are also subject to halting problem. I don't see what LLMs do that couldn't be in principle formalized as a Lean tactic. (IMHO LLMs are just learning rules - theorems of some kind of fuzzy logic - and then try to apply them using heuristic search to satisfy the goal. Unfortunately the rules learned are likely not fully consistent and so you get reasoning errors.)