IME, LLMs are completely incapable of reasoning about anything remotely difficult. All you'll get are proofs by assertion, not anything rigid you can trust.
Most proof assistants do a good job with autogenerating a (deterministically correct) proof given a careful description of the theorem. Working on integrating this into mainstream languages seems much more worthwhile than training an LLM to output maybe-correct proof-seeming bits of text.
The problem is the training corpus tends towards mediocre code. But with an agentic loop that analyzes the code against those criteria and suggests changes then I think it might be possible. I wouldn't try to get it to generate that right off the bat.
In any other industry the “worker class” would be sabotaging the machines.
In the merry software world, the challenges of improving our potential replacements are far too interesting and satisfying to leave room for any worry about consequences! :)
IME, LLMs are completely incapable of reasoning about anything remotely difficult. All you'll get are proofs by assertion, not anything rigid you can trust.
Most proof assistants do a good job with autogenerating a (deterministically correct) proof given a careful description of the theorem. Working on integrating this into mainstream languages seems much more worthwhile than training an LLM to output maybe-correct proof-seeming bits of text.
The problem is the training corpus tends towards mediocre code. But with an agentic loop that analyzes the code against those criteria and suggests changes then I think it might be possible. I wouldn't try to get it to generate that right off the bat.
I was thinking the same thing!
In any other industry the “worker class” would be sabotaging the machines.
In the merry software world, the challenges of improving our potential replacements are far too interesting and satisfying to leave room for any worry about consequences! :)