Recent discussions around AI-generated mathematical papers have raised difficult questions about verification, attribution, authorship, and even about what it will mean to do mathematics in the coming years. I do not want to enter into the merits of any particular recent case. Instead, I would like to propose something constructive. Over the past month, with the help of a few friends and colleagues, I have been developing a project called ProofForum:
The idea is simple: if AI systems are going to produce an increasing amount of mathematics, then perhaps we need a new kind of mathematical space in which those results can be openly examined, discussed, corrected, attributed, and eventually validated by mathematicians. I do not think the existing mechanisms of mathematical publication were designed for what may be coming.
Generation is not verification #
Suppose someone asks an AI system to work on an open problem. After hundreds or perhaps thousands of prompts, the system produces an argument that appears to prove a new theorem.
Who has actually contributed what?
There is the person who chose the problem, designed the prompts, guided the exploration, and selected the final argument. There is the AI system that generated the mathematical text. There may then be another mathematician who spends several days understanding the argument, finds a gap, repairs it, rewrites the proof, checks the references, and eventually becomes convinced that the theorem is true.
These are very different contributions. Our traditional notion of authorship does not fit this situation particularly well, and I suspect this will become increasingly common. This is part of the motivation for ProofForum. Instead of treating an AI-generated proof as something whose credibility rests primarily on the person who happened to generate it, why not expose it to a broader mathematical community?
A result could gradually acquire something resembling collective mathematical confidence. People could identify gaps, propose corrections, point out that a result is already known, simplify an argument, explain its central idea, connect it to existing literature, or eventually certify that the proof appears to be correct. It should resemble a “Git Hub” of proofs.
In other words, verification could itself become a visible mathematical contribution.
We may soon generate more mathematics than we can read #
There is another, very practical problem. As mathematical AI systems improve, many researchers may independently ask them to attack the same problems. Each researcher may spend substantial computational resources exploring hundreds or thousands of variations, only for several groups to rediscover essentially the same argument. This seems wasteful. A public repository of AI-generated mathematical results could reduce this duplication. Before spending a large amount of computation attacking a problem, one could see what has already been generated, what has been checked, what has failed, and what remains uncertain.
We might save computation, time, and perhaps even a little water along the way. More importantly, we might begin to build a shared mathematical memory of what the machines have already tried.
I have already submitted some AI-generated papers to ProofForum claiming solutions to problems from the Kourovka Notebook (a compendium of open problems in Group Theory). I have not checked every detail of these arguments myself; in fact, that is partly the point of the experiment.
Perhaps someone who cares about one of these problems will read the proof and find it correct. Perhaps someone will find an error. Perhaps the result is already known. Perhaps an argument buried inside the proof is interesting even if the theorem itself is not.
All of these outcomes would be useful information.
Why not simply put everything in Lean? #
There is an obvious response to the verification problem: formalize the results. I agree that proof assistants such as Lean are extraordinarily valuable, and I expect formal verification to become an increasingly important part of mathematics.
There is now also Palomar, the registry of Lean-verified mathematics, which provides infrastructure for recording and checking formally verified results. This seems to me an important development. But I do not think formal verification solves the entire problem. A proof can be formally correct without yet being mathematics that humans can understand, teach, remember, reuse, or build intuition from. This distinction matters enormously.
As mathematicians, we usually want more from a proof than a certificate that a theorem is true. We want to know why it is true. We want to recognize the trick. We want to see which hypothesis is really doing the work. We want to understand which part of the argument might generalize. We want to be able to explain it to a student.
Sometimes the most valuable thing in a paper is not even its main theorem, but an argument hidden on page twelve that another mathematician later recognizes as useful in a completely different context.
A formal proof is excellent at certifying logical correctness. But mathematical exposition has another function: it transmits understanding between human beings. I do not want us to lose that.
The humanization problem #
At the moment, many AI-generated mathematical arguments require what I would call humanization. The underlying idea may be correct. The proof may even be very close to correct. But someone still has to understand it, reorganize it, remove irrelevant detours, repair missing steps, connect it with the literature, and explain the argument in a form that another mathematician can actually learn from.
This work should not be regarded as merely cosmetic. It may become one of the central mathematical activities of the AI era. If an AI produces fifty pages proving a theorem and a mathematician turns those fifty pages into a transparent five-page argument whose central mechanism can be understood and reused, that mathematician has made a real intellectual contribution.
Likewise, if someone discovers that the AI proof contains an elegant lemma that has applications elsewhere, extracting and explaining that lemma is mathematics. We therefore may need new conventions of attribution.
Perhaps the person who generates a result, the person who verifies it, and the person who turns it into understandable mathematics should not automatically receive the same kind of credit. But all of these contributions may deserve to be recorded.
A platform such as ProofForum could experiment with ways of making these roles visible.
What happens to students? #
For me, this is the deeper question. Suppose that in ten or twenty years a substantial part of new mathematics is first produced by AI systems and then stored primarily as machine-verifiable formal proofs. How will the next generation learn mathematics from it?
How does a graduate student learn group theory if an increasing fraction of the newest arguments exist mainly as enormous formal objects?
Mathematics is not transmitted simply by transmitting theorem statements and certificates of correctness. We learn mathematics by reading proofs. We learn how mathematicians choose definitions. We learn which examples matter. We learn standard tricks. We learn when an argument is natural and when it is miraculous. We slowly acquire mathematical taste.
A proof is not merely evidence that a proposition is true. It is also a pedagogical object and a cultural object.
If AI dramatically increases the production of mathematical results, the problem of exposition becomes more important, not less. Someone will have to decide which results matter. Someone will have to explain them. Someone will have to connect them. Someone will have to turn machine-produced proofs into mathematics that can live in the minds of human beings. Otherwise we risk constructing an enormous mathematical library whose books have technically all been verified but which fewer and fewer people can actually read.
AI as a tool for mathematicians #
There is a fear, which I understand very well, that mathematicians will gradually become tools used by AI systems rather than AI systems remaining tools used by mathematicians.
If our role becomes simply to choose problems for machines, run computations, and report whatever comes out, I can understand why many mathematicians would find that deeply unsatisfying. But I do not think the solution is to hand over the final remaining stage of our understanding of the proof to the machine as well. The distinction I want to preserve is not between “human mathematics” and “AI mathematics.” It is between mathematics that humans can understand and mathematics that exists only as an artifact produced and checked by machines. Formal verification can tell us that an argument is correct.
It cannot replace the mathematical community deciding why the argument is interesting, what it teaches us, how it relates to other mathematics, or how it should be explained to the next generation. These are different tasks. And perhaps ProofForum could provide one place where that second process happens.
A collective problem requires a collective response #
We may be entering a period in which the production of mathematical material becomes larger than what any individual mathematician can reasonably absorb.
This could become chaotic. But it could also lead to new forms of collaboration.
One mathematician may generate a candidate solution. Another may verify a difficult lemma. Someone else may recognize a known theorem that simplifies half the argument. Another person may formalize it. Another may rewrite the proof conceptually. A specialist may explain its relationship with existing literature. Eventually a coherent piece of mathematics may emerge from contributions distributed across many people and machines.
Perhaps this sounds strange according to our present conventions.
In a few years it may sound completely normal.
If we build the right infrastructure, AI-generated mathematics might become more than an endless source of additional papers. It could allow machines to handle technical searches, preliminary computations, routine reductions, or enormous combinatorial explorations, while mathematicians spend more of their time identifying important questions, discovering conceptual structures, explaining ideas, and connecting apparently unrelated phenomena.
Of course, I am implicitly assuming that AI will not eventually do all of those things better than us as well.
At this point, who knows?
But whatever happens, I think there is value in building institutions that preserve mathematics as a shared intellectual activity rather than allowing mathematical production to become a collection of isolated interactions between individuals and machines.
An experiment #
ProofForum is only an experiment.
I do not claim that it is the solution to these problems. Perhaps the right system will look very different. Perhaps existing institutions will evolve. Perhaps entirely new conventions will emerge. But I think we should start experimenting now.
ProofForum is free and open. There are no fees, subscriptions, or paywalls. That matters to me. Mathematics has always depended on an extraordinary culture of sharing ideas, and I would like whatever infrastructure emerges around AI-generated mathematics to preserve that openness as much as possible.
I would be very interested in criticism, suggestions, and alternative ideas. I would also be happy to hear from anyone interested in helping develop ProofForum, whether technically or mathematically.
The arrival of increasingly capable AI systems could fragment the mathematical community. It could make us more isolated, more defensive, and more reluctant to share. I hope we choose the opposite direction. If machines allow us to produce mathematics on a scale we have never seen before, then perhaps we will need each other more than ever: to verify it, organize it, explain it, teach it, and decide what is worth remembering.
The point is not to resist formal verification, nor to resist AI. It is to make sure that formal verification does not become the only language in which tomorrow’s mathematics survives. Mathematics should remain something that can be understood by mathematicians. And, above all, something that one human being can still explain to another.
If this idea resonates with you, I would be very happy to have you participate in ProofForum: by reading a proof, leaving a comment, pointing out an error or a known result, improving an argument, or contributing your own AI-assisted mathematical experiments. Even a small contribution can help turn machine-generated output into mathematics that is easier to trust, understand, and reuse.
Received 1 September 2026.