AI & Maths watch GitHub

Archived edition

Updates on artificial intelligence for mathematical research, proof discovery and formal verification, with links to papers, code and tools.

Research updatesSelect an entry to read more

3 entries · 9 linked sources Partial coverage
Lean experts propose a quality-controlled route to formalizing most of mathematics Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, and Adam Topaz Published: 4 sources

A joint Xena essay argues that large-scale AI autoformalization should optimize for reusable mathematical infrastructure rather than raw theorem counts. It identifies concrete components of that program: human-curated Mathlib as the foundation; vetted statements through Formal Conjectures and the Annals Challenge; expert roadmaps and AI review in Tau Ceti; source-to-library conversion in Formal Frontier; and Palomar metadata plus Comparator checks for standalone projects. The proposed operating principles include avoiding duplication, generalizing for reuse, public review, continuous Lean and Mathlib compatibility, documentation, literature links, and mathematician-led governance.

Research relevance:

This is an unusually concrete workflow document for research mathematicians deciding where AI-generated Lean code can become durable infrastructure. It distinguishes statement auditing, kernel acceptance, provenance, library design, and downstream usability, and names projects where contributors can supply expert roadmaps, review, or compute.

Claim status:
Published proposal and progress report by experienced formalization researchers. The authors report current sizes and outputs for Tau Ceti and Formal Frontier and propose that most mathematics could receive useful formal representations within three years. Those project metrics and the three-year forecast are author claims, not independent certification; this digest did not compile or execute any Lean artifact.
Limitations:
The essay is advocacy and a program of work, not a benchmark study or proof that the proposed scaling strategy will succeed. AI adversarial review is not equivalent to independent human scrutiny. Formal correctness also does not by itself establish faithful correspondence with an informal theorem, mathematical novelty, good exposition, or reusable library design.

Sources & further reading

Link to this entry
SAIR soft-launches Open Math OS for collaborative mathematical AI workflows Terence Tao and the Foundation for Science and AI Research Published: 2 sources

Open Math OS has entered an early soft launch, offering academic users interfaces to hosted open mathematical models. Tao says the initial service hosts DeepSeek V4.1 Flash, Kimi K3, and GLM 5.3 Flash and is intended for tasks including medium-sized Lean formalization, mathematical discussion, and summarization. A notable workflow choice is the use of team accounts whose members can see one another's prompts. SAIR is also seeking partners to post-train a more specialized open mathematics model.

Research relevance:

The service may provide research groups with a shared, non-commercial-facing workspace for exploratory formalization and mathematical discussion. Shared prompt histories could make AI-assisted work easier to inspect, reproduce, and coordinate within a team.

Claim status:
Directly read soft-launch announcement and live project website. Claims about supported tasks and relative model capability are SAIR's own descriptions; no independent evaluation or Lean execution was performed.
Limitations:
This is an early, capacity-limited service using donated compute. Access is being granted to academic requesters rather than being guaranteed publicly, allocations may change, and the hosted models are described by Tao as roughly a year behind the frontier and unsuitable for current one-shot research-problem solving. Privacy, retention, reproducibility, and benchmark details were not established from the consulted pages.

Sources & further reading

Link to this entry
Visual Lean introduces a drag-and-drop interface for the Natural Number Game Autumn Mapes Published: date not established3 sources

Timothy Gowers announced Visual Lean on 2026-10-16 as an interface isomorphic to the established Natural Number Game but operated by clicking and dragging rather than typing Lean commands. The accessible application is aimed at newcomers learning the proof-state and tactic structure of Lean. The original public release date could not be established, so the publication date is left unknown rather than inferred from the announcement.

Research relevance:

Although primarily educational, the interface explores a practical research-tool question: whether direct manipulation can reduce the syntax barrier to interactive theorem proving. Gowers described it as the beginning of a wider interface project, which could matter for onboarding mathematicians and designing more intuitive formal-reasoning environments.

Claim status:
The dated announcement was read directly in the supplied X API feed, and the application URL was corroborated by public indexing. The claim that it is isomorphic to the Natural Number Game is Gowers's description; this digest did not test the application or inspect its implementation.
Limitations:
The application page could not be read successfully through the web tool, no official repository or technical documentation was found, and no independent usability evaluation was located. It is a learning interface, not an automated prover, autoformalizer, research result, or independently checked formalization.

Sources & further reading

Link to this entry
Coverage and limitations
  • Window checked: 2026-10-15 20:00 CEST through 2026-10-17 08:00 CEST. Public web searches and directly readable primary pages included Xena, Terence Tao's What's New, Open Math OS, Lean and GitHub pages, arXiv, Simon Frieder's blog, and linked project sites. Search-engine discovery is not exhaustive, and some pages may not yet have been indexed.
  • Direct X API collection was available for all 15 supplied X accounts. Posts were present for @__alpoge__, @wtgowers, @thomasfbloom, @alexkontorovich, @Leonard41111588, @boazbaraktcs, and @EpochAIResearch; the other supplied X feeds returned no posts. Replies and reposts were excluded, collection was bounded, cached posts could be included, and neither the exact pagination cap nor remaining API budget was supplied. No account was reported skipped. Empty feeds do not establish inactivity, and API resolution did not independently verify identity.
  • The supplied X posts were read directly through the provided API data. Other X material, including the post linked by Levent Alpöge, could not be read directly and was treated only as an unresolved lead. The terse 'Found!!!!' post was excluded because its mathematical subject and claim could not be verified from an accessible primary source.
  • The Bluesky feed for @xenaproject.bsky.social was successfully checked with a cap of 300 posts and returned no posts; replies and reposts were excluded. This does not establish inactivity. Direct Mathstodon collection failed with an HTTP error after a check capped at 300 posts, so Terence Tao's Mathstodon timeline was unavailable.
  • The official Visual Lean application returned an internal reading error through the web tool, although its exact URL and the dated announcement were accessible through the supplied direct X feed and indexed public references. The original launch date and repository were not established. LeanGraphSearch, arXiv:2610.22339, was excluded because its original submission at 2026-10-15 17:55 UTC preceded the window by about five minutes, despite being indexed during the research period. Previously reported Lean 4.35 and verified-kernel material was not repeated.

Requested coverage window: 2026-10-15T20:00:01.872228+02:00 — 2026-10-17T08:00:01.931342+02:00.

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

Archives 55
Older editions (25)