Soluciones del reto 21 de Lean 4: Las subsucesiones tienen el mismo límite que la sucesión. jaalonso.github.io/calculemus/p...

#RetoLean4 #LeanProver #ITP #Math

Weekly reads: Sep 28 – Oct 4, 2026. jaalonso.github.io/vestigium/po... #AI4Math #Agda #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #RocqProver

Proving at scale for universal algebra. ~ João Araújo, Jan Hula, Mikoláš Janota, Edmond W. H. Lee, Bartosz Naskrecki. people.ciirc.cvut.cz/~janotmik/ma... #LeanProver #ITP #AI4Math

Formalising linear elliptic PDE theory in Lean 4. ~ Alejandro José Soto Franco, Kobe Marshall-Stevens. arxiv.org/abs/2609.325... #LeanProver #ITP #Math

A Lean formalization of the Hamilton-Perelman proof of the three-dimensional Poincaré conjecture. ~ Ziyang Qin, Yuan Liao, Ayush Khaitan, Bennett Chow. arxiv.org/abs/2609.338... #LeanProver #ITP

Papers with Lean: arXiv papers that use Lean. paperswithlean.com #LeanProver #ITP

What did the Lean proof of Fermat's Last Theorem formalize? ~ Justin Asher. justinasher.me/what-did-the... #LeanProver #ITP #AI4Math

Formalize everything, now! ~ Justin Asher. justinasher.me/formalize-ev... #LeanProver #ITP #AI4Math

The Odlyzko–Poonen conjecture on irreducibility of random polynomials. ~ Constantin Kogler. arxiv.org/abs/2609.26771 #LeanProver #ITP #AI4Math

#RetoLean4: Soluciones del reto 17 (Las sucesiones convergentes están acotadas). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

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

Complement activation. Chronic inflammation. Immune-meditated pathways across cytopenias.

Tomorrow, join a free webinar to learn how targeting shared immune mechanisms may improve outcomes in #ITP, #wAIHA, and beyond.

📅 Sept 30 · 10 AM EDT
Register at👇
https://ow.ly/UmIN50ZSEs1

#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