New maths journal to require Lean-verified proofs
Confirmed
Status
- Claim
Confirmed
- Our reporting
- High confidence
- Importance
- 3 of 5
- Last verified
- 18 October 2026
Your AI and this story
- GPT-6 Astra170 days after its cutoff
- Claude Opus 5.5109 days after its cutoff
- Gemini 4 Argon200 days after its cutoff
- Grok 4.7139 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 109 days before it.
Key facts
- Guest post ‘Starting a new journal’ by Shaoming Guo on Tao’s ‘What’s new’ blog, 17 Oct 2026 (signed off by Tao as a guest post)
- Acceptance rule: ‘To be accepted, a paper will need to have its proofs formally verified in Lean.’ Reason given: with LLM-assisted proofs ‘the potential for subtle, hard-to-detect errors is a growing concern’
- Refereeing values: ‘We place far greater value on how much a paper deepens our understanding of its results and proofs’ than on priority of discovery; open access
- Not stated: journal name, editorial board, fees, launch date, or how the Lean verification will be checked; the post asks for community input and ‘ideas for substantially different visions of future journals’, adding ‘A single journal is unlikely to accommodate every worthwhile idea’
- Same day Tao listed his recent AI talks and interviews (Caltech ‘Math 2.0’ lecture Oct 9, Numberphile ‘No More Heroes’ Oct 15, NYT interview “‘I’m on a War Footing’: Terry Tao and the Crisis in Math” Oct 16, UCLA magazine ‘The Tao of Tao’ Oct 6)
What happened
After OpenAI’s mass release of AI-generated manuscripts in early October and a wave of AI-assisted proofs on arXiv, a group of mathematicians led by Shaoming Guo used Terence Tao’s widely read blog to announce a new journal built around two rules: proofs must be formally verified in Lean before acceptance, and refereeing should reward understanding over priority. The post is a call for discussion, not a launch: it gives no name, editors or date. We did not find Guo’s institutional affiliation on the page itself, so we leave it out.
Why it matters
It is the first announced research journal (that we know of) to make machine-checked proofs a condition of publication, a direct response to AI-generated mathematics arriving faster than human referees can check it. Lean verification checks the logic but not whether the formal statement matches the claimed theorem (see the Lean kernel soundness bug entry), so how the journal checks statements will matter.
Sources
4 sources from 3 sites. Numbers match the chips in the text.
4 sources: 2 primary, 2 press
Primary
- Terence Tao’s blog: Starting a new journal (guest post by Shaoming Guo, Oct 17, 2026)terrytao.wordpress.com, official
- Terence Tao: Some of my recent talks and interviews (Oct 17, 2026)terrytao.wordpress.com, official
Press
- NYT: ‘I’m on a War Footing’: Terry Tao and the Crisis in Math (Elisabeth Bumiller, Oct 16; paywalled, not read)nytimes.com, press
- UCLA magazine: The Tao of Tao (Stuart Wolpert, Oct 6)newsroom.ucla.edu, press
Changes
- Filed (read both Tao blog posts)