#Calculemus: Demostraciones con Lean 4 del Reto 9 (Unicidad del límite). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

#Calculemus: Demostraciones con Lean 4 del Reto 7 (La composición de funciones inyectivas es inyectiva). jaalonso.github.io/calculemus/p... #LeanProver #Math

#Calculemus: Demostraciones con Lean 4 del Reto 6 (teorema del emparedado). jaalonso.github.io/calculemus/p... #LeanProver #Math

Mechanizing Gödel's incompleteness theorems and provability logic. ~ Shogo Saitou, Mashu Noguchi. arxiv.org/abs/2609.13780 #LeanProver #ITP #AI4Math

Stable singularity of the Euler equations on ℝ³. ~ Adarsh Ganeshram, Valentin Duruisseaux, Anima Anandkumar. arxiv.org/abs/2609.108... #AI4Math #LeanProver #ITP

Henstock-Kurzweil gauge integral in the non--gaussian regime: a machine-verified construction. ~ Yuri N. Berdinsky. arxiv.org/abs/2609.107... #LeanProver #ITP

A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs. ~ Shenghao Yang, Yanyan Dong. arxiv.org/abs/2609.105... #LeanProver #ITP #AI4Math

Lean metaprogramming etudes: execution is elaboration. ~ Philip Zucker. www.philipzucker.com/elab_lean/ #LeanProver #ITP #FunctionalProgramming

Readings shared: 7-13 September, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #ITP #IsabelleHOL #LeanProver #LeanProver#ITP #Logic #Math

A four-valued graph model for conflict resolution: core framework and a machine-checked formalization in Lean 4. ~ Yukiko Kato. arxiv.org/abs/2609.11174 #LeanProver#ITP #Math

The Kolmogorov–Arnold representation theorem (in Lean 4). ~ George A. Constantinides. geoconuk.github.io/lean-misc-ma... #LeanProver #ITP #Math

Navier-Stokes and Lean. ~ Lance Fortnow. blog.computationalcomplexity.org/2026/09/navi... #LeanProver #AI4Math

A counterexample to a problem of Pommerenke on convex functions in the class Σ. ~ Yuankai Guo, Xiaozhe Hu. arxiv.org/abs/2609.042... #LeanProver #ITP #Math

Statistical theory in the age of machine-assisted mathematics: rethinking how theory is made and taught. ~ Pietro Coretto. arxiv.org/abs/2609.044... #LeanProver #ITP #Math

A Lean 4 formalization of Scott's continuous lattices (1972). ~ Lars Warren Ericson. arxiv.org/abs/2606.307... #LeanProver #ITP #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

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