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 · 4 linked sources Partial coverage

October 3, 2026: an AI-assisted combinatorics preprint supplies a proof and verification artifacts, while two mathematicians offer concrete guidance on research practice. Social-media archival coverage remains incomplete.

Research updatesSelect an entry to read more

AI-assisted preprint improves a lower bound for isosceles-free grid subsets Yukai Song Published: 2 sources

Song presents a proof that an n by n integer grid contains an isosceles-free subset of size at least a constant times n sqrt(log log n / log n), for sufficiently large n. Equally spaced collinear triples are forbidden too. The argument applies Cooper and Mubayi's sparse hypergraph coloring theorem using geometric degree and codegree bounds, improving PatternBoost's stated lower guarantee by a factor of order sqrt(log log n). The paper documents AI suggestions, human route selection, proof repairs and finite verification, with ancillary code and results.

Research relevance:

A concrete combinatorial result accompanied by a useful research-workflow case study: check theorem hypotheses explicitly and test whether a verifier detects deliberately omitted degenerate cases.

Claim status:
A proof is available in the preprint. The author reports AI assistance under human direction and agreement between separate finite enumerators for n from 2 through 12. These computations support implementation consistency, not the asymptotic theorem. No Lean formalization or independent proof verification was established.
Limitations:
The bound does not determine the asymptotic order of the extremal function. An earlier internal draft already contained the result. Version 1 was submitted at 01:07:54 UTC on October 3, within the Paris window; a secondary index mentions an October 6 update, which is not treated as target-day news. Neither the proof nor ancillary code was independently checked here.

Sources & further reading

Link to this entry
Idrissi proposes research logbooks and separate credit for results and explanations Najib Idrissi Published: 1 source

Idrissi describes using LLMs for references, unfamiliar mathematics, code, counterexamples and proof attempts. He recommends recording significant prompts, model versions, failed approaches, interventions and checks. For formal proofs, he emphasizes checking that the statement matches the intended mathematics and inspecting its assumptions. He proposes distinguishing publication of a supported result from later work explaining its mechanism, with explicit attribution of mathematical contributions.

Research relevance:

Practical guidance for maintaining auditable AI-assisted research records and recognizing conceptual explanation as a substantial mathematical contribution.

Claim status:
A dated essay reporting personal experience and proposing research and publication practices; it announces no theorem or checked formalization.
Limitations:
The recommendations are not evaluated experimentally. The current page refers to discussions published after October 3, so it may contain later edits; this digest does not treat those references as evidence available on the target day.

Sources & further reading

Link to this entry
Taback reports useful AI assistance with lemma repair and paper organization Jennifer Taback Published: 1 source

In a guest post on Tao's blog, Taback reports that AI has helped repair an incorrect lemma, reorganize a paper and suggest unfamiliar research directions, while failing to solve her longstanding problems. She advocates disclosing research tools and taking responsibility for verification, understanding and explanation before dissemination. She also argues that second proofs remain valuable and that changing professional standards must account for mathematicians at teaching-intensive institutions.

Research relevance:

A concrete account of incremental assistance in ordinary mathematical research, with implications for collaboration, mentoring and evaluation.

Claim status:
A dated first-person research-practice report. The mathematical examples are not supplied as proofs or independently assessed results.
Limitations:
No prompts, model versions, manuscripts or reproducible artifacts accompany the reported successes. This is qualitative experience and professional guidance, not a capability benchmark.

Sources & further reading

Link to this entry
Coverage and limitations
  • Public web searches reconstructed October 3, 2026, the Paris civil day. Included dates come from original blog pages or arXiv submission history, not indexing dates.
  • Read the original arXiv abstract and HTML version of Yukai Song's preprint, Najib Idrissi's Proofs and Prompts essay, and Jennifer Taback's guest post on Terence Tao's blog. No proof was independently verified and no code or Lean was executed.
  • Consulted Tao's blog and its Mastodon aggregation, Xena at https://xenaproject.wordpress.com/, Gowers's blog, and official personal or institutional pages for Alpöge, Armstrong, Bloom, Litt, Kontorovich, Charton, de Moura and Barak. Also opened official Lean, Project Numina, Harmonic, Axiom and Epoch AI websites. Project Numina returned no readable text; Bubeck's former Microsoft profile redirected to a general directory.
  • Identity checks were incomplete: official pages supplied some social links, but not every supplied handle could be corroborated. Date-specific searches covering all supplied X handles returned no results. Other searches exposed indexed profiles and third-party mirrors, which were treated only as leads; no complete October 3 X timeline was accessible. Buzzard's supplied Bluesky identity was not corroborated, and complete Mathstodon and Bluesky archives were not consulted.
  • Excluded Cogentic as older material found during reconstruction: its primary-source search result gives a September 30 submission, despite October 3 secondary coverage. Excluded the already reported October 2 Meta announcement, older Navier–Stokes commentary recirculated on October 3, and a Zenodo record originally published September 30 but modified October 3.
  • Secondary indexes suggested additional formalization leads, but no original October 3 publication date was established for them. They were excluded. Blog pages were read in their current form; later edits cannot be ruled out without archived snapshots.

Requested coverage window: 2026-10-03T00:00:00+02:00 — 2026-10-04T00: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)