New journal proposed on Tao's blog would require Lean verification for every proof under the motto "understanding over priority," alongside eight choices that separate a golden age from a dark age for math in the AI era

Human peer review can no longer keep up with the mathematical results AI is producing. Mathematicians have now responded with a proposal for a new journal. In "Starting a new journal", published on Terence Tao's blog on October 17, the proposed journal would require every proof it publishes to be formally verified in the proof assistant Lean. Its motto is "understanding over priority." The next day, October 18, the blog published "Will it be a golden age or a dark age for mathematics and science?", which argues that eight choices will decide whether mathematics and science in the AI era enter a golden age or a dark age.

Over the past month, the mathematical community had already set up two ways of handling AI results: a rule change on the Erdős problems site, and a repository called Hexagon. The journal proposal goes a step further and makes verification a condition of submission.

Machine verification as a gate before peer review

The journal's biggest departure from existing journals is that it would hand the question of whether a proof is correct to a machine first. Every submitted proof would be expected to be formalized in Lean already. That would free human referees from checking the logic line by line. Instead, they could spend their time on what a result reveals, why it matters and how it connects to earlier work.

The motto "understanding over priority" says where the journal places a paper's value: not in who got the result first, but in what readers can understand from it. Now that AI can produce proofs in bulk, being "the first to solve it" suddenly counts for much less. The motto can be read as writing that shift into the journal's editorial policy.

Why "priority" became a problem

The past month in the mathematical community explains where the motto comes from.

On October 6, OpenAI posted 722 manuscripts from an unnamed internal model to GitHub (719 after later retractions and other changes). The next day, a sign error was found in a manuscript on the algebraicity of Weil classes, and the company withdrew it along with two manuscripts that relied on it, three in all. About 42% of the manuscripts are said to be formalized in Lean. In a guest post on Tao's blog dated October 12, Sophie Huiberts called the release "just plain bad work." She said the sourcing of ideas was handled improperly, the work was sliced into small pieces, and the proofs were extraordinarily hard to decipher.

Pressure over priority is also changing how human researchers behave. In a guest post on September 22, Antonio Auffinger wrote that, for fear that someone would feed their ideas to an AI, junior researchers were rushing papers out and colleagues were holding back from posting to arXiv. AI has flooded the field not only with results but with anxiety over who gets there first. The new journal's motto responds to that directly.

The Erdős site, Hexagon, and a journal that requires verification

These venues have been built from slightly different directions.

On October 6, Thomas Bloom changed the rules of the Erdős problems site, which had become a place where AI-generated proofs with no explanation were posted to claim priority. The site dropped its "solved/unsolved" labels and its count of solved problems, and stopped crediting results to whoever solved them, human or AI. It now favors human-readable explanations and linked Lean proofs. Scrapping the credit count in favor of understanding and verification lines up directly with the new journal's motto.

Also on October 6, Ben Antieau launched Hexagon, a nonprofit repository that collects results obtained with help from LLMs. It accepts work written entirely by an LLM and does not require formal verification. Instead, it limits each submitter to one submission per day. Submissions began arriving on October 12–13, and most carried a "mostly AI-generated" label.

Taken together, the three show a division of labor. Hexagon is a holding area for unverified AI results. The Erdős site has changed its rules to stop tallying credit and to favor verification and explanation. The new journal would publish only work that has passed verification. Systems built on verification are stacking up in stages.

What requiring Lean means, and the weaknesses that remain

The argument that AI proofs should be verified in Lean before they are published is not new. Kevin Buzzard made it in "To grieve, or not to grieve?" on October 1. "How to Formalize All of Mathematics" by Avigad, Buzzard, Commelin and others, which Tao highlighted on October 16, also dealt with balancing speed and understanding in large-scale autoformalization. The new proposal turns those discussions into something concrete: a submission requirement.

Verification in Lean is not absolute, however. In a guest post on October 9, Thomas Hales looked back on a run of soundness bugs in Lean's kernel in July and August ("Summer of Soundness Bugs"). He proposed cross-checking proofs across about 25 independent Lean kernels, formally verifying the kernel itself and shoring up the underlying theory. He also noted that no complete proof of relative consistency for Lean's type theory has yet been published. A journal that requires verification would also have to take on trust in that foundation.

Another issue is how far formalization reaches. Lean's libraries are far deeper in some fields than in others. If every proof must be verified, results from fields where formalization is further along will be easier to publish. Which fields to accept, and how, will be a major question in designing the journal.

Choices, not capability, will decide "golden age or dark age"

The October 18 post treats the future of mathematics and science in the AI era as a question of what the community chooses, not of how capable the technology is. As the title suggests, it argues that eight choices will decide between a golden age and a dark age.

That view follows the position Tao took in "Math 2.0" on October 10. There he criticized what he saw as too much emphasis on having AI solve open problems automatically, and called for keeping humans at the center, with AI supporting human understanding and the mathematical community. The journal proposal from the day before can be seen as an attempt to answer at least one of those choices with an institution: whether to judge work by who publishes first or by whether it is understood.

Open questions

Much remains to be decided before the proposal becomes a working journal. Who will edit it, and who will pay for it? Who will bear the work of formalizing in Lean? And how should submissions in which AI did the formalization be credited as the authors' work?

On funding, there is the $15 million program that the Simons Foundation, Anthropic and OpenAI launched on October 15. It uses open calls to support systems for evaluating AI-assisted results and for developing community standards, and could be a possible backer. "It should be the community that leads the discussion of how these tools are evaluated, adopted and used, not any single company or institution," said Simons Foundation President Spergel. The journal proposal is an attempt by mathematicians themselves to build a venue for that discussion, with verification as its starting point.