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.

Research updatesSelect an entry to read more

2 entries · 4 linked sources Partial coverage
Public AI-assisted Lean package claims the three Joshi–Rust Thue–Morse first-occurrence formulas dot (OpenAI), as credited in the package; submitted by ZestyDingo473 Published: 3 sources

A package dated October 4 claims formulas for the earliest starting positions of longest monochromatic arithmetic progressions in the Thue–Morse sequence at differences 2^n+1, 2^(2n)−1 and 2^(2n+1)−1. It supplies Lean source and an informal carry/desubstitution argument. The first family requires n≥2; the excluded n=1 case has earliest start 45. The other families require n≥1 and n≥0 respectively.

Research relevance:

A concrete research claim in combinatorics on words, with public artifacts addressing maximality and exclusion of every earlier start rather than merely displaying long progressions.

Claim status:
Available proof package and claimed Lean checking. The public record identifies the result as a candidate with review pending and does not claim human expert endorsement. Its October 4 submission and the README's explicit date establish the publication date.
Limitations:
The current record includes later moderation and edits. Its retrospective notes report an author-supplied build receipt, no repository CI, and no independent rebuild by the registry. Those notes are later assessments, not necessarily information available on October 4. I read the README and headline source but did not audit the complete proof or execute Lean. Broader classifications for arbitrary differences are not claimed.

Sources & further reading

Link to this entry
Córdoba and Martínez-Zoroa explain the mathematical scope of fluid singularity claims Diego Córdoba and Luis Martínez-Zoroa; guest post hosted by Terence Tao Published: 1 source

The specialists explain vortex-layer cascades and distinguish instantaneous regularity loss from blow-up after a period of unique classical evolution. Their discussion places recent AI-assisted announcements alongside earlier analytical and computer-assisted work. It separates forced ordinary Navier–Stokes blow-up from unforced Euler blow-up and explains why their own forced fractional Navier–Stokes construction, with dissipation exponent below approximately 0.093, does not extend directly to the ordinary exponent 2.

Research relevance:

Useful technical context for evaluating headline PDE claims: forcing regularity, initial-data smoothness, finite energy and the precise dissipation operator materially change the problem.

Claim status:
Dated expert exposition and contextual scrutiny, not certification of the announced AI-assisted proofs. The authors explicitly say they cannot yet make a substantive comparison between OpenAI's constructions and their cascade methods.
Limitations:
The underlying results and the referenced September 8 announcement predate this edition; the new contribution is the October 4 exposition. No new solution or checked formalization is established by this post. Tao discloses AI use to convert the post's file format, which does not establish AI involvement in its mathematical arguments. I did not verify the cited proofs.

Sources & further reading

Link to this entry
Coverage and limitations
  • Reconstructed the Paris civil day October 4, 2026 through public web searches performed on October 7. Only sources explicitly dated October 4 were included; indexing dates were not treated as publication dates.
  • Read the dated fluid-dynamics guest post on Terence Tao's official blog, the Thue–Morse submission record, and its linked GitHub README and headline Lean source. The submission record contains later edits; its current verification commentary cannot all be attributed to October 4.
  • Consulted What's New, Proofs and Prompts, Gowers's Weblog and Xena. Kevin Buzzard's Imperial website establishes https://xenaproject.wordpress.com/ as his blog. Consulted official websites for Lean, Axiom, Epoch AI, Harmonic, Daniel Litt and Thomas Bloom; these checks did not establish all supplied social-account identities.
  • Date-specific searches covering the supplied X handles returned no usable target-day posts. Direct access to Gowers's X profile failed. Indexed profile and third-party mirror snippets were seen but were not accepted as dated announcements or identity certification. Exhaustive X access was unavailable.
  • Tao's official blog links to its Mastodon aggregation, but the direct Mathstodon profile yielded almost no readable content. Buzzard's supplied Bluesky account and the remaining personal X identities were not independently authenticated. Project Numina's website yielded no readable text; attempted personal-site access for Barak, Alpöge and Armstrong failed.
  • Excluded October 4 secondary recaps of earlier Meta, AGMAI and Fermat formalization announcements, generic explainers, and unrelated educational benchmarks. No new target-day correction to the supplied previous entries was established. No source code was executed and no Lean build or proof verification was performed.

Requested coverage window: 2026-10-04T00:00:00+02:00 — 2026-10-05T00:00:00+02:00.

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

Archives 58
Older editions (28)