Formal or not formal? That is the question in AI for theorem proving.

Summary

So it’s an interesting time for computers-doing-mathematics. A couple of interesting things happened in the last few days, which have inspired me to write about the question more broadly. First there is the question on whether computers will ever prove interesting research-level mathematical theorems autonomously at all, which is really hard to answer right now, although clearly a lot of people are betting on “yes”. I personally am unsure: I’ve seen what can currently be done, and can’t quite extrapolate that far once you cut through the hype. I am however far more optimistic about AI tools becoming useful helpers to mathematics researchers, and this is one of the things which motivates my current work (trying to teach Lean a lot of research-level definitions, theorem statements and proofs ). But whether they beat us or just help us, one can still ask what an autonomous theorem-proving tool will look like. Let’s initially take a gigantic step down from research level mathematics and talk instead about problems which can be solved by smart schoolchildren, namely those on the International Mathematics Olympiad (IMO). I wrote recently about the attempts by AI on the 2025 IMO but all you need to know here is that there were four attempts which were made public: two of them were using language models to write proofs in English (which were then graded by humans); let’s call this the “informal approach”. The other two were using a language model/Lean hybrid set-up; let’s call this the “formal approach”. Lean is a computer proof checker or interactive theorem prover; it checks mathematical arguments at a superhuman level. In this hybrid setup, the language model writes proofs in Lean’s language which are then checked automatically by Lean; once Lean says the proofs are correct, humans only need to check that the statements have been translated correctly into Lean, although that is an important part of the process. Worries about the non-formal approach. What worries me mostly about the non-formal approach is the horror stories I am hearing from journal editors. Mathematics journals are being spammed with LLM-generated papers, which are becoming more and more plausible-looking, and sometimes the use of LLMs is not even revealed in the paper. I want to flag some differences between mathematics papers generated by LLMs and those generated by humans: 1. LLMs are sycopha…