The readings shared in Bluesky on 29 January 2026 are:

• Formalising the Bruhat-Tits tree. ~ Judith Ludwig, Christian Merten. #ITP #LeanProver
• Formalizing Fermat, Lecture 1. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Formalization of brownian motion in Lean. ~ David Ledvinka. #ITP #LeanProver
• New automation for Lean: grind. ~ Kim Morrison. #ITP #LeanProver
• MRiscX: Certified RISC-V interpreter with Hoare logic as a DSL. ~ Julius Marx. #ITP #LeanProver
• Simpler do proofs with mvcgen. ~ Sebastian Graf. #ITP #LeanProver
• Formalizing value distribution theory of complex analysis. ~ Stefan Kebekus. #ITP #LeanProver #Math
• The Lean module system. ~ Sebastian Ullrich. #ITP #LeanProver
• Formalization of the Ionescu-Tulcea theorem in Mathlib. ~ Etienne Marion. #ITP #LeanProver #Math
• A bottom-up approach to formalisation in the FLT project. ~ Salvatore Mercuri. #ITP #LeanProver #Math
• The universal divided power algebra. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• CSLib: The Lean Computer Science Library. ~ Fabrizio Montesi. #ITP #LeanProver
• Formalisation of CW complexes. ~ Hannah Scholz. #ITP #LeanProver #Math
• Formalizing Schwartz functions and tempered distributions. ~ Moritz Doll. #ITP #LeanProver #Math
• lean-lsp-mcp: Tools for agentic interaction with Lean. ~ Oliver Dressler. #ITP #LeanProver #AI
• Tactics for the linear-bitwise fragment of bitvectors. ~ Siddharth Bhat. #ITP #LeanProver
• Coinductive predicates in Lean. ~ Wojciech Różowski. #ITP #LeanProver
• The state of Lean. ~ Leo de Moura. #ITP #LeanProver
• Locally nameless lambda calculi. ~ Chris Henson. #ITP #LeanProver
• Hopf algebras, affine group schemes and all of that. ~ Yaël Dillies. #ITP #LeanProver #Math
• Verification of model-checking techniques in Lean. ~ Atticus Kuhn. #ITP #LeanProver
• Teaching real analysis as a video game. ~ Alex Kontorovich. #ITP #LeanProver #Math
• Autoformalization for physics and engineering with Lean. ~ Leopoldo Sarra. #ITP #LeanProver
• Formalization of homotopy theory in Lean. ~ Joël Riou. #ITP #LeanProver #Math
• The sphere packing project. ~ Sidharth Hariharan, Seewoo Lee, Chris Birkbeck. #ITP #LeanProver
• Internal projectivity of the sequence space in Lean. ~ Jonas van der Schaaf. #ITP #LeanProver #Math
• Formal verification of Rust cryptographic code in Lean with Aeneas. ~ Son Ho. #ITP #LeanProver
• Better living through metaprogramming. ~ Thomas R. Murrills. #ITP #LeanProver
• Verified computation of real asymptotics. ~ Vasilii Nesterov. #ITP #LeanProver
• Lessons from the Carleson project. ~ Floris van Doorn. #ITP #LeanProver
• The Mathlib initiative. ~ Johan Commelin. #ITP #LeanProver
• Formalizing class field theory. ~ Michał Mrugała. #ITP #LeanProver #Math
• Aristotle, an AI theorem prover using Lean. ~ Alex Best. #AI #Math #AI4Math #ITP #LeanProver #Aristotle
• Nori's construction in Lean. ~ Sophie Morel. #ITP #LeanProver
• Writing proofs by clicking. ~ Jovan Gerbscheid. #ITP #LeanProver
• What's new in the Lean standard library. ~ Markus Himmel, Sofia Rodrigues. #ITP #LeanProver
• Metaprogramming the next generation of testing tools. ~ Harry Goldstein. #ITP #LeanProver
• LeanTutor: Towards a verified AI mathematical proof tutor. ~ Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade. #AI #Math #AI4Math #ITP #LeanProver #LLMs
• Competitive pure functional languages. ~ Sami Badawi. #FunctionalProgramming #Hakell #LeanProver
• Verified non-recursive calculation of Beneš networks applied to Classic McEliece. ~ Wrenna Robson, Samuel Kelly. #ITP #LeanProver
• A generalization of Boppana's entropy inequality. ~ Boon Suan Ho. #ITP #LeanProver
• Swap distance (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL
• Thinking machines: Mathematical reasoning in the age of LLMs. ~ Andrea Asperti, Alberto Naibo, Claudio Sacerdoti Coen. #AI #Math #AI4Math #LLMs