Readings shared April 24, 2026
The readings shared in Bluesky on 24 April 2026 are:
- Deep Vision: A formal proof of Wolstenholmes theorem in Lean 4. ~ Alexandre Linhares. #LeanProver #ITP #AI4Math
- Discover and prove: An open-source agentic framework for hard mode automated theorem proving in Lean 4. ~ Chengwu Liu et als. #LeanProver #ITP #AI4Math
- Formalising the Bruhat–Tits tree. ~ Judith Ludwig and Christian Merten. #LeanProver #ITP
- Formally verified patent analysis via dependent type theory: Machine-checkable certificates from a hybrid AI + Lean 4 pipeline. ~ George Koomullil. #LeanProver #ITP #AI4Math
- Lean: First steps. ~ Tariq Rashid. #LeanProver #ITP #Math
- Lecture «Interactions of AI with research math and formalization» at Newton Insitute (Cambridge). ~ Alex Kontorovich. #AI4Math #LeanProver #ITP
- Logique propositionnelle (dans Lean). ~ Sebastien Lahaye. #LeanProver #ITP #Logic
- Understanding tool-augmented agents for Lean formalization: A factorial analysis. ~ Ke Zhang, Patricio Gallardo, Maziar Raissi, Sudhir Murthy. #LeanProver #ITP #AI4Math
- grind best practices. ~ Chris Henson. #LeanProver
- Formal primal-dual algorithm analysis. ~ Mohammad Abdulaziz, Thomas Ammer. #IsabelleHOL #ITP
- Just type it in Isabelle! AI agents drafting, mechanizing, and generalizing from human hints. ~ Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens, Mohammad Abdulaziz, Andrei Popescu, Dmitriy Traytel. #IsabelleHOL #ITP #AI4Math
- A Rocq formalization of simplicial Lagrange finite elements. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. #RocqProver #ITP #Math
- A constructive proof of Rice's theorem and the halting problem via Hilbert's tenth problem. ~ Jonathan Brossard. #RocqProver #ITP #Math
- A formal proof of the Sands-Sauer-Woodrow theorem using the Rocq prover and mathcomp/ssreflect. ~ Jean-Philippe Chancelier. #RocqProver #ITP #Math
- On reasoning-centric LLM-based automated theorem proving. ~ Yican Sun, Chengwei Shi, Hangzhou Lyu, Yingfei Xiong. #RocqProver #AI4Math
- Do LLMs game formalization? Evaluating faithfulness in logical reasoning. ~ Kyuhee Kim, Auguste Poiroux, Antoine Bosselut. #AI4Math #LeanProver #ITP #Autoformalization
- The fall of the theorem economy (How AI could destroy mathematics and barely touch it). ~ David Bessis. #AI4Math #LeanProver #ITP
- Why not just use Lean?. ~ Lawrence Paulson. #ITP #Nqthm #HOL #CoqProver #IsabelleHOL #LeanProver #AI4Math
- The Haskell Unfolder Episode 54: Not quite monads. #Haskell #FunctionalProgramming
- Introduction to computational logic. ~ Ryan Kavanagh. #Logic #Math #CompSci
- All elementary functions from a single binary operator. ~ Andrzej Odrzywołek. #Math
- EML: una función para generarlas a todas. ~ Miguel Ángel Morales. #Math
- Matemáticas en la era de la IA: demostraciones rápidas, comprensión lenta. #AI4Math
- Reseña de «The fall of the theorem economy (How AI could destroy mathematics and barely touch it)». #AI4Math #LeanProver #ITP