Readings shared March 4, 2026
The readings shared in Bluesky on 4 March 2026 are:
- When AI writes the world’s software, who verifies it? ~ Leonardo de Moura. #AI #LeanProver #ITP
- Formalising sphere packing in Lean. ~ Chris Birkbeck, Sidharth Hariharan, Gareth Ma, Bhavik Mehta, Seewoo Lee, Maryna Viazovska. #LeanProver #ITP #Math
- The sphere packing project (Post 1: The story). ~ Chris Birkbeck Sidharth Hariharan Seewoo Lee. #LeanProver #ITP #Math
- Completing the formal proof of higher-dimensional sphere packing. #LeanProver #ITP #AI4Math
- The purpose of proofs. ~ Lance Fortnow. #LeanProver #ITP #AI4Math
- SorryDB: Can AI provers complete real-world Lean theorems? ~ Austin Letson et als. #LeanProver #ITP #AI
- ReasBook is a Lean 4 project for formalizing mathematics from textbooks and research papers. #LeanProver #ITP #Math
- A formally verified constructive proof of the consistency of Peano arithmetic using ordinal assignments. ~ Aaron Bryce, Rajeev Goré. #CoqProver #ITP #Math
- Mechanizing the proof of a borrow calculus. ~ Alban Reynaud Michez. #RocqProver #ITP
- Monuses and heaps. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming