New proofs of weak normalization for propositional logic. ~ S P Suresh. arxiv.org/abs/2609.14314 #LeanProver #ITP #Logic

Sage: Formalization with semantic correction. ~ Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni, Xiang Zhou, Wengping Deng, Liang Zhang. arxiv.org/abs/2609.35790 #LeanProver #ITP #AI4Math

A constructive ATLAS of finite simple groups in Lean. ~ Gerald Höhn. arxiv.org/abs/2609.35847 #LeanProver #ITP #AI4Math

Proofs without nominals: Gödel's ontological argument, its shallow embedding, and the open questions of the Monatshefte Notes. ~ Christoph Benzmüller. arxiv.org/abs/2609.36279 #IsabelleHOL #LeanProver #ITP

What mathematical specification connects their treatment of Navier–Stokes / nonlocal PDE structure, and where do the constructions differ?

Use the Galerkin reading point here for reference: readingpoint.app/galerkin/

📚🚦🛹
#LeanLang #LeanProver

#RetoLean4: Soluciones del reto 20 (Si aₙ → L y M es una cota superior de aₙ, entonces L ≤ M). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

#RetoLean4: Enunciado del reto 21 (Las subsucesiones tienen el mismo límite que la sucesión). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Formalization of the Poincaré Conjecture in Lean 4. ~ PKU AI for Math team. frenzymath.com/news/poincar... #LeanProver #ITP #Math

Formalizing Carleson's theorem in Lean. ~ Lars Becker et als. arxiv.org/abs/2609.313... #LeanProver #ITP #Math

Readings shared: 21-27 September, 2026. jaalonso.github.io/vestigium/po... #AI4Maht #Agda #ITP #IsabelleHOL #LeanProver #LogicProgramming #Math #Prolog #RocqProver

zazbrown.com/research/pap... #Math #AI4Math #LeanProver

Visual Lean: An accessible interface for Lean 4 proofwriting. ~ Autumn Mapes. aitp-conference.org/2026/abstrac... #LeanProver #ITP

Formalization of Langlands’s first main lemma for local epsilon factors. ~ Fukuhiro Ueda. hal.science/hal-05746185... #LeanProver #ITP #AI4Math

#Vestigium: Formalización del libro "Calculus" de Spivak en Lean 4. jaalonso.github.io/vestigium/po... #LeanProver #ITP #AI4Math

Lean 4 formalization of Michael Spivak's "Calculus" (covering both the 3rd and 4th editions). ~ Jon-Erik G. Storm. github.com/stormj-UH/sp... #LeanProver #ITP #AI4Math

#Calculemus: Demostraciones con Lean 4 del Reto 15 (Existe un k ∈ ℕ tal que, para todo n ∈ ℕ, (n + k)² ≤ 2ⁿ⁺ᵏ). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Formalization of Harder-Narasimhan theory. ~ Yijun Yuan. arxiv.org/abs/2509.19632 #LeanProver #ITP #AI4Math

#Calculemus: Demostraciones con Lean 4 del Reto 14 (Para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Gödel's and Scott's variants of the ontological argument in Lean 4. ~ Christoph Benzmüller. arxiv.org/abs/2609.268... #LeanProver #ITP #AI4Math

A formalization at large (Laver function in Lean). ~ Leheng Chen, Bin Dong, Jiedong Jiang, Zhiyuan Zhang. frenzymath.com/blog/laverta... #LeanProver #ITP #Math