Readings shared September 28, 2026
The readings shared in Mastodon on 28 September 2026 are:
- A formalization at large (Laver function in Lean). ~ Leheng Chen, Bin Dong, Jiedong Jiang, Zhiyuan Zhang. #LeanProver #ITP #Math
- Formalization of Harder-Narasimhan theory. ~ Yijun Yuan. #LeanProver #ITP #AI4Math
- Gödel's and Scott's variants of the ontological argument in Lean 4. ~ Christoph Benzmüller. #LeanProver #ITP #AI4Math
- Formalization of Langlands’s first main lemma for local epsilon factors. ~ Fukuhiro Ueda. #LeanProver #ITP #AI4Math
- Lean 4 formalization of Michael Spivak's "Calculus" (covering both the 3rd and 4th editions). ~ Jon-Erik G. Storm. #LeanProver #ITP #AI4Math
- Visual Lean: An accessible interface for Lean 4 proofwriting. ~ Autumn Mapes. #LeanProver #ITP
- A formalisation of a special case of the union-closed conjecture in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. #IsabelleHOL #ITP
- A formalisation of a special case of the union-closed conjecture in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. #IsabelleHOL #ITP
- Deterministic context-free languages are closed under complementation (Hopcroft and Ullman). ~ Kaan Taskin, Tobias Nipkow. #IsabelleHOL #ITP
- Notes on Gödel’s and Scott’s variants of the ontological argument. ~ Christoph Benzmüller, Dana Scott. #IsabelleHOL #ITP
- The Teichmüller-Tukey lemma (in Isabelle/HOL). ~ Vithor Lindermann Kraisch, Luiz Gustavo Cordeiro. #IsabelleHOL #ITP #Math
- Verified QBF solving in Isabelle/HOL: a trustworthy baseline for mechanised quantified boolean reasoning. ~ Axel Bergström, Tjark Weber. #IsabelleHOL #ITP
- Verifying numerical methods with Isabelle/HOL. ~ Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster. #IsabelleHOL #ITP #AI4Math
- Verifying numerical methods with Isabelle/HOL. ~ Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster. #IsabelleHOL #ITP #Math
- Work bounds for strongly joinable balanced binary search trees (in Isabelle/HOL). ~ Marco Haucke. #IsabelleHOL #ITP
- Formal verification of tilt estimation using the Rocq prover. ~ Reynald Affeldt, Lynda Bentoucha, Yoshihiro Ishiguro, Holger Thies. #RocqProver #ITP
- The logic of Bunched implications is undecidable, mechanized in Rocq. ~ Dominique Larchey-Wendling. #Rocq #ITP
- A mechanized formalization of MicroKanren in Agda. ~ Eduardo Henke, Rodrigo Ribeiro. #Agda #ITP
- "Be a Grothendieck!" — On AI and mathematics. ~ Gil Kalai. #AI4Math
- AI and mathematical research. ~ Claudia Alfes, Thomas Nikolaus, Andreas Thom. #AI4Math
- All the math we will not see. ~ Alessandro Della Corte. #AI4Math
- El miedo al lado oscuro de la IA en la comunidad matemática. ~ Anabel Forte Deltell. #AI4Math
- Navigating the AI crisis: a humble guide for students. ~ Tarik Aougab. #AI4Math
- New math + AI developments in fluid mechanics. ~ Javier Gomez-Serrano. #AI4Math
- ProofForum: Keeping AI-generated mathematics human. ~ Marco Trombetti. #AI4Math
- Summit on PhD math education in the age of AI. #AI4Math
- The scientific debate over AI in mathematics. ~ Oswaldo Royett. #AI4Maht
- ¿Realmente ha resuelto OpenAI el "problema matemático del milenio" de Navier-Stokes? ~ Víctor Javier Llorente Lázaro. #AI4Math
- Enscryerypt: Encrypt and decrypt files with Scryer Prolog. ~ Markus Triska. #Prolog #LogicProgramming
- ¿Qué son los números reales? II. ~ Esteban Martínez. #Math
- #Calculemus: Demostraciones con Lean 4 del Reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). #LeanProver #ITP #Math
- #Calculemus: Demostraciones con Lean 4 del Reto 14 (Para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). #LeanProver #ITP #Math
- #Calculemus: Demostraciones con Lean 4 del Reto 15 (Existe un k ∈ ℕ tal que, para todo n ∈ ℕ, (n + k)² ≤ 2ⁿ⁺ᵏ). #LeanProver #ITP #Math
- #Calculemus: Demostraciones con Lean 4 del Reto 19 (Las sucesiones convergentes son sucesiones de Cauchy). #LeanProver #ITP #Math
- #Vestigium: Formalización del libro "Calculus" de Spivak en Lean 4. #LeanProver #ITP #AI4Math
- #Vestigium: Lista de usos y expectativas de la IA en matemáticas. #AI4Math