Readings shared January 29, 2026
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