AI & Maths watch GitHub

Retrospective research digest

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

At a glance3 entries · 7 linked sources Partial coverage

September 11, 2026: two dated Lean formalization registry records and a joint declaration on AI and mathematical research. Public social-media archives and direct access to the registry evidence were incomplete.

Research updatesSelect an entry to read more

Kolmogorov–Arnold superposition formalization receives a dated registry record George A. Constantinides Published: 2 sources

Palomar registered a Lean formalization of three superposition statements, including the Lorentz–Sprecher form. The inner functions are chosen before the continuous function being represented, preserving their universality for the dimension. This formalizes classical mathematics rather than announcing a new superposition theorem.

Research relevance:

A substantial analysis formalization with an explicit statement surface. Its quantifier order illustrates a crucial issue when auditing autoformalized mathematical claims.

Claim status:
The indexed registry record reports successful Comparator, Lean-kernel and independent nanoda checks at 16:20 UTC, plus an automated comparison of the formal and informal statements.
Limitations:
The detailed registry evidence was available through indexed extracts, not readable direct page content. Checking reports were not independently audited. Automated statement review is not human peer review; the extent of AI involvement in constructing this proof was not established.

Sources & further reading

Link to this entry
Lean record reports a resolution of Gallardo’s polynomial-substitution conjecture Brandon Yates Published: 3 sources

A Palomar registration reports a formal resolution of Luis H. Gallardo’s December 23, 2019 conjecture: for n ≥ 2, 1 + X + … + Xⁿ is irreducible over GF(2) exactly when 1 + P + … + Pⁿ is, with P = X² + X + 1. The repository states the same result. The registry describes a proof using the classical Artin–Schreier trace criterion.

Research relevance:

A concrete finite-field problem with public Lean artifacts, a compact statement surface and an explicit treatment of the excluded boundary case n = 1.

Claim status:
The indexed registry record reports Comparator, Lean-kernel and nanoda checks at 21:35 UTC, with automated statement review. The repository claims a resolution; the original OEIS comment establishes the conjecture’s provenance.
Limitations:
The registration is the dated news; the conjecture is older. Detailed checking evidence was seen in indexed extracts and was not independently replayed. The trace mechanism is classical, and AI participation in proof construction was not established.

Sources & further reading

Link to this entry
Fields medallists publish a joint declaration on AI and mathematical understanding Joint signatories, including Terence Tao Published: 2 sources

A Severe Misalignment of AI in Mathematics argues that benchmark-driven theorem production can undermine attribution, readable exposition, student development and the transmission of mathematical ideas. The declaration acknowledges AI’s potential to accelerate research while asking researchers and companies to prioritize understanding and the integration of results into mathematical practice.

Research relevance:

A substantive intervention concerning how AI-assisted results should be explained, credited and developed into reusable mathematics. This is a new joint declaration, distinct from the earlier individual essays and fluid-equation announcements.

Claim status:
Publication and text are established by the original dated declaration and Tao’s same-day blog post. Its arguments are positions on research practice, not independent certification of any AI-generated theorem.
Limitations:
The live declaration has accumulated additional signatories since publication. Its broad claims about mathematical capability do not establish the correctness or significance of particular proofs, and it supplies no new mathematical result.

Sources & further reading

Link to this entry
Coverage and limitations
  • Reconstructed the Paris civil day September 11, 2026, using public web searches and original sources consulted on October 7. Registry verification times of 16:20 and 21:35 UTC both fall within the requested Paris day.
  • Read the dated declaration on Terence Tao’s blog and its English text at mathandai.org. The declaration website now lists additional signatories; its current list should not be treated as the original September 11 list.
  • Opened both Palomar records, but their pages returned only minimal application text. Detailed registration dates, mathematical statements and verification claims were visible in indexed source extracts. Read the related GitHub repository pages and the original OEIS conjecture; did not inspect every proof file or archived checking report.
  • Confirmed Xena as Kevin Buzzard’s blog through his Imperial College webpage. Its September 4 Fermat’s Last Theorem post is older material found during reconstruction and was excluded. The previously supplied September 7–10 entries were not repeated.
  • Checked personal or institutional websites for Gowers, Bloom, Litt, Kontorovich, Charton, Barak and de Moura, and official sites for Lean, Harmonic, Axiom and Epoch AI. Barak’s and de Moura’s sites supplied social-account links, but fetching those accounts failed. Other supplied handles were not all independently authenticated and were not used as certified identities.
  • Direct X access to Project Numina, Harmonic and Axiom returned 403 errors. Project Numina’s website returned no readable text; leanprover.org failed, while lean-lang.org was accessible. Attempted Alpöge, Bubeck and Armstrong homepage URLs failed. Tao’s Mathstodon profile returned a JavaScript shell. Buzzard’s Bluesky archive was not consulted. Coverage of the supplied accounts is therefore incomplete and does not establish that they posted nothing.
  • Excluded con-leche because a later de Moura presentation dates its release to September 10. Excluded benchmark claims found only in secondary briefings without an established September 11 primary announcement. Search crawl dates, later reviews and event dates were not treated as publication dates.
  • No proof was independently verified and no Lean code was executed.

Requested coverage window: 2026-09-11T00:00:00+02:00 — 2026-09-12T00:00:00+02:00.

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

Archives 32
Older editions (2)