Proof by Clicking
When I went to university, I took a class in Mathematical Logic. This course had just introduced a new pedagogical tool: Alfa, a computer program that helped us students write logical proofs. The program didn’t do any proving itself; it only helped with the administrative details of putting together a correct proof. It showed the possible next steps and hypotheses and we could focus on what next step to choose and simply click that button.
As part of the examination we were given a whole bunch of proofs to do as homework, including some optional theorems which were considered very hard to prove. What we found was that all these proofs were simple and could be proven with a very simple method: just pick the most obvious next step (an “introduction rule”) and when you get stuck, look at the hypotheses and pick a promising one (it was typically relatively easy because these proofs required few hypotheses). Once we figured out this method, all the theorems became easy to prove, even the supposedly hard ones.
Our professor was quite taken aback by this simple method and how effective it was. He had assumed that many of the “harder” theorems required deep insight. What the tool revealed was that the insight was not in the final proof. It had been in trying to keep many of the details in one’s head, to develop new mental models to be able to manage all the complexities of the proof. Alfa cleared all that away, and what was left was just of hitting the button for the next obvious step. The professor dubbed this method “proof by clicking”.
On October 6th 2026, OpenAI released an enormous batch of proofs of theorems, conjectures, and improvements on bounds that have eluded mathematicians for a long time1. All the proofs were generated by AI, with human supervision. This is an extraordinary feat by OpenAI. It is also, for the mathematicians reading these papers, an almost unreadable one. The papers provide no helpful intuition, the structure of the proofs is labyrinthine and the references often don’t make any sense. 2
Many of the proofs released by OpenAI are formalized in Lean, a proof tool similar in spirit to Alfa, only vastly more powerful. The same bargain is on offer: the system handles the organization and the administrative details, and always shows you a way forward. I’m not claiming these proofs are merely “proof by clicking”; they construct new objects no amount of clicking could conjure. What connects them is the end product: proofs that are mechanical, and that leave you no more enlightened than before. My professor’s surprise was that clearing away the toil revealed how little of the insight had been in the proof itself. The worry now runs the other way: if the toil is where insight lives, what happens when we remove all of it?
Where does that leave us humans? We now live in a new reality where AI can prove theorems with superhuman capability. We’ve come to almost expect AI-powered breakthroughs in math on a regular basis. These breakthroughs all have a very similar pattern: they are all proofs of existing conjectures, or improvements on bounds for existing problems. We have yet to see any new and interesting conjectures by an AI. Nor have we seen AI come up with new and interesting abstractions, or potential new subfields of mathematics. That seems to be reserved for humans, at least for now.
I fear that human mathematicians might become worse at coming up with new conjectures. The intuition that is required to establish a relevant hypothesis is generated in all the toil of trying to prove theorems. The sweat and headache that goes into understanding a problem well enough to prove it is the very thing that feeds the intuition. If we leave the hard proving to AI, how will we develop the intellectual muscles to be able to come up with conjectures?
Will AI be able to also provide the conjectures and new mathematical subfields in the future? Betting against AI has been a good way to lose money lately. But AI seems to struggle with things like relevance and coming up with genuinely new abstractions. Whether AI can achieve that requires a whole other essay, at the very least. In the meantime, mathematicians should continue to do the hard work of proving theorems. The important part is to train the math muscles so as to not become too weak.