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 glance4 entries · 5 linked sources Partial coverage

Four substantive publications dated September 18, 2026 were identified: a claimed AI-assisted Conway proof, a candid Frankl-conjecture workflow report, an open mathematical-model initiative, and a proposal for rewarding mathematical explanation. Archival social-media coverage remains incomplete.

Research updatesSelect an entry to read more

Abramov publishes a claimed AI-assisted proof of Conway's refinement conjecture Dan Abramov Published: 2 sources

Abramov describes a month-long project using Claude and OpenAI models to obtain a Lean proof of Conway's refinement conjecture for omnific integers: ab = cd should admit factors e, f, g, h with a = ef, b = gh, c = eg and d = fh. He links public proof artifacts and explains failed approaches, conditional lemmas mistaken for completed results, and difficulties turning formal code into readable mathematics.

Research relevance:

A research-level algebraic claim accompanied by formal artifacts and an unusually informative account of AI research management. The conjecture concerns the integer part of the surreal numbers.

Claim status:
Author-announced proof with available Lean code. Abramov reports successful mechanical checks but explicitly says mathematicians have not independently verified the proof.
Limitations:
Formal correctness and correspondence with the intended conjecture require separate assessment. The current article mentions checks added after release; their target-day availability is not established. The linked registry record predates this article, so September 18 dates the write-up rather than necessarily the discovery.

Sources & further reading

Link to this entry
Hanson reports what worked and failed in an agent-based attack on Frankl's conjecture Eric P. Hanson Published: 1 source

Hanson publishes an exploratory workflow combining LLM agents, Lean, Julia, SAT solving, integer programming and a collection of explicit counterexamples. He reports refutations of 80 proposed statements using 105 families, while clearly stating that Frankl's union-closed sets conjecture remains open. The most useful lessons concern bounded searches reported as exhaustive, stale claims, checks sharing bugs with the code they test, and computation replacing mathematical ideas.

Research relevance:

A practical account of organizing computational mathematical exploration, preserving negative results, and separating experimental output from actual progress on an open problem.

Claim status:
First-person experimental report, not a solution of Frankl's conjecture. A possible improvement concerning Karpas's theorem is presented as an agent claim requiring the author's further understanding or formal verification.
Limitations:
The September 18 publication reformats slides from a September 3 talk and describes work begun in August. Reported counts and subsidiary results were not independently checked; the author characterizes the project as a short initial exploration.

Sources & further reading

Link to this entry
Tao announces SAIR's initiative for open mathematical models and research tools Terence Tao and SAIR Foundation Published: 1 source

Tao announces an accelerated initiative to develop openly licensed model weights, code, training methods and reproducible evaluations for mathematical work. Its proposed first phase targets understanding arguments, checking references, exploring examples, coding and formalizing proofs. The announcement commits to documented data permissions, explicit consent for using researchers' data, and public community governance.

Research relevance:

Potential infrastructure for inspectable and independently runnable mathematical assistants, with evaluation aimed at everyday research usefulness and sustained cost.

Claim status:
Initiative announcement and invitation for participation. The post does not establish a released model, working tool or demonstrated mathematical result.
Limitations:
Partners, detailed implementation and governance remained under development in the announcement. Promised openness and research utility were prospective commitments rather than independently demonstrated capabilities.

Sources & further reading

Link to this entry
Sanderson proposes treating mathematical explanation as a research deliverable Grant Sanderson Published: 1 source

In a guest essay on Tao's blog, Sanderson proposes recognizing explanations that show how one could discover an argument, including explanations requiring specialist expertise. He suggests identifying open exposition problems, developing assessment standards, and asking students to defend their understanding through talks. Earlier AI-assisted primitive-set work serves as an example of the additional value created by interpreting, simplifying and extending a generated proof.

Research relevance:

Concrete proposals for graduate training and research evaluation when producing a proof and developing transferable mathematical understanding become increasingly distinct tasks.

Claim status:
Dated opinion essay with practical proposals; no new theorem or formalization is announced.
Limitations:
Assessment of explanation remains partly subjective. The mathematical examples concern earlier results and are context, not September 18 discoveries. The proposals had not been demonstrated as an adopted evaluation system.

Sources & further reading

Link to this entry
Coverage and limitations
  • Reconstructed September 18, 2026, the Paris civil day, using public web searches conducted on October 7, 2026. Included entries have original sources explicitly dated September 18; exact publication times were generally unavailable.
  • Read Dan Abramov's original article, its linked GitHub repository, Eric P. Hanson's original workflow report, and Terence Tao's two dated posts. Read Tao's September archive and Kevin Buzzard's Xena blog; confirmed the Xena address through Buzzard's Imperial College webpage.
  • Consulted official websites for Levent Alpöge, Daniel Litt, Boaz Barak, Lean, Numina, Harmonic, Axiom and Epoch AI. These checks did not authenticate every supplied social handle or establish complete historical timelines. The remaining supplied personal-account identities were not independently established through official websites.
  • Searches for dated X material returned sparse results and third-party mirrors. No complete September 18 timeline was accessible for the supplied accounts; Mathstodon and Bluesky histories were not consulted. Absence from search results does not establish absence of announcements.
  • Palomar pages opened with only a minimal JavaScript shell. Detailed registry claims were visible in indexed search text, not readable registry records. The several-complex-variables registration was therefore excluded pending fuller primary-source access.
  • Excluded introductory Lean tutorials as insufficiently substantial. Also excluded a dated secondary digest's claim of ten new OpenAI mathematical solutions because an original September 18 announcement was not established; a Purdue seminar listing concerned an earlier non-sofic-group result and did not establish a new publication that day.
  • Excluded earlier supplied items and out-of-window material, including the Lean Kernel Challenge post dated September 16 and Xena's Fermat formalization post dated September 4. Search-index crawl dates were not treated as publication dates.
  • Current article and repository contents may incorporate later edits. Where an article explicitly identifies additions made after release, these were not treated as evidence of what was available on September 18. No code was executed and no proof or Lean build was independently verified.

Requested coverage window: 2026-09-18T00:00:00+02:00 — 2026-09-19T00: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)