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