#Calculemus: Demostraciones con Lean 4 del Reto 11 (Si aₙ converge a L, entonces |aₙ| converge a |L|). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Napoleon's theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Napo... #IsabelleHOL #ITP #Math

Fast chinese remaindering via product trees (in Isabelle/HOL). ~ Manuel Eberl. isa-afp.org/entries/CRT_... #IsabelleHOL #ITP

Palindromic length in free groups: reflections, noncrossing matchings, and Catalan. ~ Junjie Liao. arxiv.org/abs/2609.170... #LeanProver #ITP

Formalization of Sullivan's no wandering domains theorem in Lean. ~ Ziang Li, Yusheng Luo. arxiv.org/abs/2609.160... #LeanProver #ITP #AI4Math

#Calculemus: Demostraciones con Lean 4 del Reto 10 (Si aₙ → L con L ≠ 0, entonces |aₙ| ≥ |L|/2 eventualmente). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Strong normalization for Church-style system F (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Syst... #IsabelleHOL #ITP

Greibach’s hardest context-free language (in Isabelle/HOL). ~ Tobias Nipkow. isa-afp.org/entries/Grei... #IsabelleHOL #ITP

#RetoLean4: Enunciado del reto 19 (Las sucesiones convergentes son de Cauchy). t.me/Retos_Matema... #LeanProver #ITP #Math

#RetoLean4: Soluciones del reto 18 (Convergencia del producto de sucesiones convergentes). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

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

Structuring mathematics in dependent type theory. ~ Cyril Cohen. inria.hal.science/tel-05737923/ #RocqProver #ITP #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

Monadic second-order logic in HOL: deep and shallow with automated faithfulness. ~ Christoph Benzmueller, Daniel Kirchner. arxiv.org/abs/2609.073... #IsabelleHOL #ITP #Logic

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