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