Readings shared December 2, 2025
The readings shared in Bluesky on 2 December 2025 are:
- The machine translation of Landau’s analysis of foundations in Rocq. ~ Yue Guan, Yaoshun Fu, XiangTao Meng. #ITP #Rocq #Math
- Formalization of brownian motion in Lean. ~ Rémy Degenne, David Ledvinka, Etienne Marion, Peter Pfaffelhuber. #ITP #LeanProver
- Kimina Lean server: A high-performance Lean server for large-scale verification. ~ Marco Dos Santos et als. #ITP #LeanProver #LLMs
- ProofGym: Unifying LLM-based theorem proving across formal systems. ~ Xinrui Li et als. #ITP #LeanProver #IsabelleHOL #CoqProver #LLMs
- The 5th Workshop on Mathematical Reasoning and AI at NeurIPS 2025. #AI #Math
- HERMES: Towards efficient and verifiable mathematical reasoning in LLMs. ~ Azim Ospanov et als. #ITP #LeanProver #LLMs
- How IT managers fail software projects (AI won’t solve IT’s management problems). ~ Robert N. Charette. #Software
- A formalization of functor quasi-categories in Lean 4. ~ Jack McKoen. #ITP #LeanProver #Math