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

Two substantive entries were located for October 4, 2026: a claimed AI-discovered Thue–Morse proof with public Lean artifacts, and specialist context for AI-assisted fluid singularity claims. Social-media archival coverage remains limited.

Research updatesSelect an entry to read more

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 32
Older editions (2)