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