The readings shared in Mastodon on 14 September 2026 are:

• A Lean 4 formalization of Scott's continuous lattices (1972). ~ Lars Warren Ericson. #LeanProver #ITP #AI4Math
• A counterexample to a problem of Pommerenke on convex functions in the class Σ. ~ Yuankai Guo, Xiaozhe Hu. #LeanProver #ITP #Math
• A four-valued graph model for conflict resolution: core framework and a machine-checked formalization in Lean 4. ~ Yukiko Kato. #LeanProver#ITP #Math
• A kernel-checked proof of Fuglede's conjecture for the cyclic group Z/180Z. ~ Javier Emilio Bazán Sánchez. #LeanProver #ITP #Math
• Lean 4 formalization of the Gurvich-Naumova ternary partition theorem. ~ JD Jones. #LeanProver #ITP #AI4Math
• Lean4 formalization of s-numbers (in the sense of Pietsch) and important inequalities. ~ Mario Ullrich. #LeanProver #ITP #AI4Math
• Navier-Stokes and Lean. ~ Lance Fortnow. #LeanProver #AI4Math
• SparseStack is an optimal oblivious subspace embedding. ~ Diar Heidary. #LeanProver #ITP #AI4Math
• Statistical theory in the age of machine-assisted mathematics: rethinking how theory is made and taught. ~ Pietro Coretto. #LeanProver #ITP #Math
• Steering aesop for theorem proving: learning to configure symbolic solvers via multi-source neurosymbolic feedback. ~ Kai-Yuan Jeng, Ru-Jun Wang, Wen-Tsuen Chen. #LeanProver #ITP #AI4Math
• The Kolmogorov–Arnold representation theorem (in Lean 4). ~ George A. Constantinides. #LeanProver #ITP #Math
• Two boundary-certificate proofs of the Crouzeix theorem: fiberwise Fourier recurrence and defect-Gram telescoping. ~ Qinyu Luo. #LeanProver #ITP #AI4Math
• Monadic second-order logic in HOL: deep and shallow with automated faithfulness. ~ Christoph Benzmueller, Daniel Kirchner. #IsabelleHOL #ITP #Logic
• The Földes–Hammer characterization of split graphs (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• The five platonic solids (in Isabelle/HOL). ~ Evan Finken. #IsabelleHOL #ITP #Math
• (Auto)formalization, but why? ~ Seewoo Lee. #AI4Math #LeanProver #ITP
• A 50-year-old computer-assisted proof. ~ John D. Cook. #AI4Math
• AI has solved one of math’s $1 million Millennium Prize Problems. ~ Konstantin Kakaes. #AI4Math
• AI may have just solved a million-dollar math problem. The field will never be the same. ~ Joseph Howlett. #AI4Math
• AI software completes a formal proof of Fermat’s Last Theorem. ~ David H Bailey. #AI4Math
• AutoGraphForge: Towards automated graph theory discovery. ~ Ján Pastorek. #AI4Math #LeanProver #ITP
• Clay Institute won't call Navier-Stokes solved after OpenAI proof claim. ~ Marcus Schuler. #AI4Math
• On the Navier–Stokes Millennium Prize Problem. ~ OpenAI. #AI4Math
• On the existence of non-sofic groups. ~ Andreas Thom. #AI4Math
• On the impact of AI on the mathematical practice. ~ Manuel Rivera. #AI4Math
• The Association for Human Mathematics (AHM). ~ AHM communications group. #AI4Math
• What Lean checked and Astra didn't: two kinds of verification, one week apart. ~ Scott J. McCormick. #AI4Math
• What is mathematics now, and what should it be? ~ Jeremy Avigad. #AI4Math
• What’s not new. ~ Orr Shalit. #AI4Math
• How to welcome LLM use into student research mentorship. ~ Joshua Siktar. #AI
• El teorema de Goldbach-Euler. ~ Miguel Ángel Morales. #Math