Mathematicians propose a journal that accepts only Lean-verified proofs

A group of mathematicians wants to start a journal that will not accept a paper unless its proofs are formally verified in Lean. The proposal appeared on 17 October 2026 as a guest post by Shaoming Guo on Terence Tao’s blog. The post is marked as a guest post; it is Guo’s proposal, not Tao’s.

“Several math colleagues and I are preparing to launch a new journal,” Guo writes. Beyond traditional values such as open access, the planned journal has two:

• “Prioritizing understanding over being first.” The post says the journal will “place far greater value on how much a paper deepens our understanding of its results and proofs than on whether it provides the first proof of those results.”
• “Ensuring rigor through formal verification.” The reason is AI: “As large language models (LLMs) are increasingly used to develop mathematical proofs, the potential for subtle, hard-to-detect errors is a growing concern. To be accepted, a paper will need to have its proofs formally verified in Lean.”

Lean is a proof assistant: a program that checks, step by step, that a formal proof follows from its definitions and axioms. Its community library, mathlib, holds a large body of formalized mathematics that such proofs build on.

A proposal, not a launch

The post gives no journal name, no editors, no publisher and no launch date. It is framed as the start of a discussion. Guo asks for “feedback on this proposal” and for “ideas for substantially different visions of future journals”, and warns that “combining too many requirements could place excessive constraints on authors.” The hope, the post says, is “a variety of new journals and other platforms.”

The debate around it

The next day the same blog carried a second guest post, by Francesco Maggi: “Will it be a golden age or a dark age for mathematics (and science)?” It is an opinion piece, not part of the journal proposal. Maggi writes that “LLMs seem most at home when writing proofs in Lean”, but that for hard theorems those Lean proofs can run to “hundreds of thousands of lines”, leaving “correct Lean proofs that we cannot directly read.” He argues formalization can support peer review, but “human intervention remains necessary to establish meaning, relevance, and context.”

Read together, the two posts pull at the same problem from both ends: Lean can show a proof is correct, and understanding still has to come from people. Guo’s planned journal asks for both.

Related: SAIR’s Open Math OS and the 722 math manuscripts OpenAI posted from an unreleased model.