Requiring formalisation of AI-generated proofs
Some thoughts on peer review and adversarial proof
Peer review - the process of checking each other’s work for correctness- already places huge burdens on working mathematicians. As a journal editor I am privileged to see many examples of the tremendous amount of effort and dedication that referees put in to checking to the very best of their ability that the work of their fellow mathematicians is correct.
However, referees are only human. For the most important results (in my own field the proof of Fermat’s Last Theorem springs to mind), teams of referees work on a paper, and even then it can take time for the result to be accepted by the community. Sometimes this process fails, and important published results can remain controversial. On a more pedestrian level, even published papers which are `essentially correct” can contain lemmas with missing hypotheses, proofs with significant gaps, etc. Despite this, the mathematics literature remains vastly more reliable than the literature in other parts of science, largely due to the superhuman efforts of referees.
Imagine how much worse this situation would become if mathematicians were intentionally setting out to mislead their fellows by publishing false but plausible proofs (taking a cue from the Machine Learning literature, one might call this an “adversarial proof”). No referee could ever take a reference or calculation on trust. Every `slightly incorrect’ lemma in the literature could be used to deduce the Riemann Hypothesis. Every paper would need Fermat’s Last Theorem-levels of scrutiny - and not only papers proving important results, but also every paper on which they depend. It seems clear to me that the system would immediately collapse if a significant proportion of mathematicians began to work like this.
Why do we not write adversarial proofs? It is very hard to become a research mathematician. People who make that effort do so out of passion for the subject, and are strongly incentivised not to gain a reputation for putting out incorrect proofs. This does not mean that people are not incentivised to occasionally take some shortcuts, perhaps hand-wave the proof of a lemma while secretly knowing it is not quite so straightforward; nonetheless I think there are extremely few mathematicians who would publicly announce a proof which they know to be fundamentally incorrect.
AI systems (Claude, ChatGPT, Gemini, Alethia, …) face none of these constraints or incentives. Their breadth of knowledge of the literature surpasses that of any human. Their training incentivises them to produce arguments which convince human reviewers who are usually working on very short timescales. They have no professional reputation to protect or career to maintain. These systems are strongly optimised for writing proofs that seem plausible to human readers, but only weakly optimised for correctness; in effect, these are adversarial proofs. The temptation for human authors to offload some of the work to proving tedious background lemmas to these systems is only going to grow over time, leading to such arguments spreading through the mathematical literature.
At present these systems are not so capable that human mathematicians have much difficulty checking their arguments for flaws, given a reasonable amount of effort. I would be very happy for this situation to persist, but I think we have to try to make mathematics somewhat resilient against the more advanced AI systems that are likely to arrive soon.
The problems above are not unique to mathematics. AI is able to generate increasingly reasonable-looking results in many domains, and the problem of carefully checking this output is a growing one; though perhaps mathematicians are less well-prepared for this because we are used to a particularly high level of reliability in our literature.
But a more important difference in mathematics is that we have a solution to this problem to hand, namely formalisation. In recent years writing mathematical proofs in a formal and computer-checkable language has transformed from an impractical dream to a problem of effort and logistics. A large majority of the undergraduate mathematics curriculum has already been formalised, as well as a substantial number of cutting-edge results - as I write, a large team is working on the formalisation of the proof of Fermat’s Last Theorem. It is still (at least in principle) possible to write adversarial proofs in a formal language, for example by exploiting bugs in the underlying software, but it is vastly harder than writing them in informal language, and the problem of closing off these loopholes is a large but plausibly surmountable one.
This leads to my proposal: AI-generated proofs should only be published by mathematics journals if they are accompanied by a formally-verified proof.
More concretely, when submitting a paper for publication authors should be required to declare all use of AI, and if that use extends to writing proofs then those proofs should also be accompanied by a formalised argument. Of course there are grey areas; if an AI system points out that that the proof of some lemma you need is already in the literature, it’s not reasonable to expect this to be formalised; if an AI system suggests to try applying techniques from a certain field and the author successfully implements this hint, again I would consider this basically a human argument. But if all AI use is declared then these decisions lie with referees and editors, who are better positioned than authors to make objective judgements about which parts of a proof are plausibly adversarial.
This proposal has an obvious weakness: it puts heavy demands on the honesty of authors, who are strongly incentivised to understate AI use. I hope that a strong community norm (helped by the example of leading mathematicians) would encourage many to follow this practise. But more practically, given the current state of these systems, an author who routinely submits AI generated proofs without acknowledgment runs a large risk of becoming known for unreliable work, and due to this principle of declaration the fact that the flawed arguments came from an AI will not be viewed as a valid excuse.
Another weakness is that at present not every proof can be formalised, even taking as axioms other established results from the literature. In this case one should simply flag such a proof as AI-sourced, and briefly justify why formalisation is not practical; it is then up to a referee to decide how much additional scrutiny is justified.
This is a proposal that the mathematics community (authors, journals, publishers) can choose to implement - we are not dependent on the cooperation of companies developing AI systems. It is also a proposal that may benefit the world outside mathematics; the lack of trustworthiness of AI systems is a growing issue, and improving the architecture for formally verified results might impact a range of areas (imagine if the software in a self-driving car could be proven to be correct).
This proposal will put AI systems at a disadvantage relative to humans in producing mathematical results, at least in the short-term. At present there is a vast backlog of informal mathematical literature that would need to be formalised in order to make the formalisation of all cutting-edge mathematics possible. But this is a task for which AI systems themselves are well suited - the field of autoformalisation (teaching AI systems to convert informal proofs into formal ones) is developing rapidly. I would much rather have AI systems working to check the proofs of human mathematicians than have humans working to check AI-generated proofs.
It is conceivable that AI systems will never develop much beyond where they are today. In that case this proposal will have been an over-reaction, and perhaps I will be mildly embarrassed; but this is a tradeoff that I would be delighted to accept.
Disclaimer: I am a managing editor for Compositio Mathematica and a subject editor for the Glasgow Mathematical Journal (GMJ). Compositio adheres to the Ethical Policy of the LMS, which requires the declaration of all AI use. GMJ adheres to the Cambridge University Press publishing ethics, which also require the declaration of all AI use. I wrote the note above in a personal capacity, for my editorial work I adhere to the ethical policies of the relevant journal and try not to let my own biases influence my decisions.