A Lean 4 formalization of Scott's continuous lattices (1972). ~ Lars Warren Ericson. arxiv.org/abs/2606.307... #LeanProver #ITP #AI4Math

AI has solved one of math’s $1 million Millennium Prize Problems. ~ Konstantin Kakaes. www.quantamagazine.org/ai-has-solve... #AI4Math

Hahaha, yes! Perhaps I should have added #AI4Math (or #eggbros 🤭)

What is mathematics now, and what should it be? ~ Jeremy Avigad. proofsandprompts.com/2026/09/07/w... #AI4Math

Lean4 formalization of s-numbers (in the sense of Pietsch) and important inequalities. ~ Mario Ullrich. github.com/mario-ullric... #LeanProver #ITP #AI4Math

Lean 4 formalization of the Gurvich-Naumova ternary partition theorem. ~ JD Jones. palomar-registry.org/entry.html?i... #LeanProver #ITP #AI4Math

(Auto)formalization, but why? ~ Seewoo Lee. proofsandprompts.com/2026/09/08/a... #AI4Math #LeanProver #ITP

What’s not new. ~ Orr Shalit. proofsandprompts.com/2026/09/08/w... #AI4Math

On the Navier–Stokes Millennium Prize Problem. ~ OpenAI. openai.com/index/navier... #AI4Math

AI may have just solved a million-dollar math problem. The field will never be the same. ~ Joseph Howlett. www.scientificamerican.com/article/ai-m... #AI4Math

Clay Institute won't call Navier-Stokes solved after OpenAI proof claim. ~ Marcus Schuler. www.implicator.ai/clay-institu... #AI4Math

SparseStack is an optimal oblivious subspace embedding. ~ Diar Heidary. arxiv.org/abs/2609.029... #LeanProver #ITP #AI4Math

AutoGraphForge: Towards automated graph theory discovery. ~ Ján Pastorek. arxiv.org/abs/2609.034... #AI4Math #LeanProver #ITP

Steering aesop for theorem proving: learning to configure symbolic solvers via multi-source neurosymbolic feedback. ~ Kai-Yuan Jeng, Ru-Jun Wang, Wen-Tsuen Chen. openreview.net/forum?id=Vnc... #LeanProver #ITP #AI4Math

Two boundary-certificate proofs of the Crouzeix theorem: fiberwise Fourier recurrence and defect-Gram telescoping. ~ Qinyu Luo. www.preprints.org/frontend/man... #LeanProver #ITP #AI4Math

Verification, formalisation and canonisation: formal theorem proving in the age of AI. ~ Sidharth Hariharan. thefundamentaltheor3m.github.io/beamers/tifr... #AI4Math #ITP

Li's criterion for the Riemann Hypothesis, in Lean 4. ~ Nicholas Bulka. github.com/nicholasbulk... #LeanProver #ITP #AI4Math

The global Kronecker–Weber theorem in Lean 4. ~ Naganori Yamaguchi. github.com/n-yamaguchi-... #LeanProver #ITP #AI4Math

Erdős problem #501 in Lean 4. ~ Elliot Glazer. github.com/elliotglazer... #LeanProver #ITP #AI4Math

A proof of the Regts–Sevenster conjecture, formalized. ~ William Whistler. github.com/WillWhistler... #LeanProver #ITP #AI4Math