Readings shared December 14, 2025
The readings shared in Bluesky on 14 December 2025 are:
- A rose tree is blooming (Proof Pearl). ~ Joomy Korkut. #ITP #Rocq
- A modular Lean 4 framework for confluence and strong normalization of lambda calculi with products and sums. ~ Arthur Ramos, Anjolina Oliveira, Ruy de Queiroz, Tiago de Veras. #ITP #LeanProver
- Learning about proof with the theorem prover Lean: the abundant numbers task. ~ Athina Thoma, Paola Iannone. #ITP #LeanProver #Math
- So, computers can prove theorems (in Lean), what’s next? ~ Alex J. Best. #AI #Math #ITP #LeanProver
- Lessons from the PrimeNumberTheorem+ project and real analysis game. ~ Alex Kontorovich. #ITP #LeanProver #Math
- Challenges in (auto)formalizing category theory. ~ Emily Riehl. #ITP #LeanProver #Math
- The making of Lean. ~ Leo de Moura. #ITP #LeanProver
- The Carleson project: formalization and collaboration. ~ Michael B. Rothgang. #ITP #LeanProver
- Differential geometry in Mathlib. ~ Michael B. Rothgang. #ITP #LeanProver
- Brownian motion and stochastic integrals. ~ Rémy Degenne et als. #ITP #LeanProver #Math
- Probability theory in Mathlib. ~ Rémy Degenne. #ITP #LeanProver #Math
- The Haskell Unfolder Episode 52: Bidirectional parsing and printing (of JSON). ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
- #Exercitium: Desemparejamiento de listas. #Haskell #ProgramaciónFuncional