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

#Calculemus: Demostraciones con Lean 4 del Reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Readings shared: 14-20 September, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math #RocqProver

#Calculemus: Demostraciones con Lean 4 del Reto 12 (Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ). jaalonso.github.io/calculemus/p... #LeanProver #ITP #Math

Lean-certified infinite counterexamples to written on the Wall II Conjecture 194. ~ Cameron Beeley. arxiv.org/abs/2609.191... #LeanProver #ITP #AI4Math

Descriptive complexity in Lean: completeness by first-order reductions. ~ Pierre Senellart, Anton Gnatenko. arxiv.org/abs/2609.182... #LeanProver #ITP #AI4Math

#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

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

#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