AI and Mathematics Research Watch

Research updatesSelect an entry to read more

18 Oct 2026 · 08:00 CEST1 entry · 2 linked sources Partial coverage

Shaoming Guo announces plans for a journal requiring Lean-verified proofs and prioritizing understanding Shaoming Guo; guest post hosted by Terence Tao Published: 17 Oct 20262 sources

Shaoming Guo writes that he and several unnamed colleagues are preparing a new open-access mathematics journal organized around two proposed values: papers should deepen understanding rather than merely win priority, and accepted proofs should be formally verified in Lean. The proposal is a concrete response to the growing volume of LLM-assisted proofs: it would separate deductive checking from referees’ work on exposition and mathematical understanding, although the announcement does not yet specify how theorem-statement correspondence, dependencies, axioms, or formal artifacts would be audited.

Research relevance:

This is a potentially important workflow experiment for AI-assisted research publishing. If implemented carefully, it could make machine-checkable artifacts a routine submission requirement while preserving human review for significance, explanation, attribution, and semantic alignment—the parts that Lean’s kernel does not decide.

Claim status:: Announcement of a planned journal and proposed editorial principles. The announcement was directly read on Terence Tao’s official blog, and the guest author link leads to Shaoming Guo’s academic homepage. No journal site, editorial board, call for papers, accepted proof, or operational verification process was available to inspect. This is not an independently tested publishing system.
Limitations:: The journal is described as being prepared, not launched. Its name, participating colleagues, timetable, scope, formalization standards, trusted Lean environment, policy on axioms and external dependencies, and procedure for checking that formal statements match prose claims are unspecified. Requiring a Lean proof would check a particular formal statement only under the selected environment; it would not by itself establish faithful formalization, novelty, explanatory quality, or independent peer review.

Sources & further reading

Link to this entry

Coverage and limitations

Directly read Terence Tao’s official blog homepage and both posts dated 2026-10-17, plus the linked Shaoming Guo academic homepage. Tao’s separate talks-and-interviews post mostly collects older material; its Math 2.0 material was already covered in previous editions and was not repeated.
Directly read Kevin Buzzard’s Xena blog homepage; its newest visible post was the already-covered 2026-10-16 proposal on formalizing mathematics. Kevin Buzzard’s supplied Bluesky feed returned status ok but no posts; replies and reposts were excluded and at most 300 posts were checked. An empty bounded result is not evidence of inactivity.
Directly read Simon Frieder’s official blog index, which exposed no substantive new entry in the window in the accessible page. Search results were also checked for recent AI-for-mathematics, Lean, proof, counterexample, and autoformalization material; indexed snippets were treated only as leads unless the underlying page was opened.
Terence Tao’s Mathstodon collection was unavailable because of an HTTP error. Replies and reposts were excluded and collection would have checked at most 300 posts. Tao’s official blog was available, but this does not substitute for a complete Mathstodon timeline.
The supplied X API feeds reported status ok for all 15 accounts: @__alpoge__, @scottnarmstrong, @wtgowers, @sebastienbubeck, @thomasfbloom, @littmath, @alexkontorovich, @f_charton, @leonard41111588, @boazbaraktcs, @leanprover, @projectnumina, @harmonicmath, @axiommathai, and @epochairesearch. Collection was bounded, could include cached posts, excluded replies and reposts, and API resolution did not independently verify identity. No pagination count or precise budget was supplied, so completeness cannot be assessed.
The X feeds were empty for @scottnarmstrong, @wtgowers, @sebastienbubeck, @littmath, @alexkontorovich, @leonard41111588, @leanprover, @projectnumina, @harmonicmath, and @axiommathai. Empty bounded feeds do not establish that no relevant posts existed.
Posts were supplied for @__alpoge__, @thomasfbloom, @f_charton, @boazbaraktcs, and @epochairesearch. Bloom’s image reaction, Charton’s general commentary, Barak’s terse linked reactions, and Epoch AI’s game and cybersecurity posts did not establish substantive mathematical research news. Alpöge’s “Found!!!!” post linked to an @sweis post, but the target returned HTTP 403 and searches did not identify a primary mathematical artifact; it was therefore excluded rather than interpreted speculatively.
Direct public access to X failed for the Alpöge and @sweis URLs. The supplied API text for Alpöge was read directly from the collection, but the linked @sweis post was neither directly read nor independently verified. No claim is made that any complete X timeline was consulted.
The journal announcement names neither the journal, its complete editorial group, a launch date, submission rules, nor a formal verification policy beyond requiring Lean. No code was executed and no Lean artifact was checked.

Requested coverage window: 2026-10-16T20:00:01.931342+02:00 — 2026-10-18T08:00:01.679423+02:00.

Public web research; coverage is not exhaustive. A source link is not a certification of a claim.

Archives 55

Older editions (25)