The readings shared in Bluesky on 29 April 2026 are:

• A Lean companion to «Conceptual mathematics». ~ David Kinkead. #LeanProver #ITP #Math
• A milestone in formalization: The sphere packing problem in dimension 8. ~ Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska. #LeanProver #ITP #AI4Math
• Formalizing $A_1^{(1)}$ curve neighborhoods in Lean 4. ~ Yihe Huang, Sizhe Cui, Jiaqi Wang, Jujian Zhang. #LeanProver #ITP
• Lean: extensible, scalable, trusted. ~ Leo de Moura. #LeanProver #ITP #AI4Math
• The golden thread (A formally verified three-stratum realization of the Fibonacci eigenform). ~ Richard Goodman, Vladimir Veselov. #LeanProver #ITP #Math
• ZFLean: a framework for set-level mathematics in Lean. ~ Vincent Trélat. #LeanProver #ITP #Math
• QED: An open-source multi-agent system for generating mathematical proofs on open problems. ~ Chenyang An, Qihao Ye, Minghao Pan, Jiayaun Zhang. #AI4Math
• Archimedes' cattle problem (in Isabelle/HOL). ~ Manuel Eberl. #IsabelleHOL #ITP #Math
• Nominal unification (in Isabelle/HOL). ~ Guilherme Borges Brandão, Thomas Ammer, Daniele Nantes Sobrinho, Mauricio Ayala-Rinción, Christian Urban, Maribel Fernández, Mohammad Abdulaziz. #IsabelleHOL #ITP
• Formalizing the real numbers in Homotopy Type Theory with Cubical Agda. ~ Jackson Brough. #Agda #ITP #Math
• What works and doesn't selling formal methods in industry. ~ Mike Dodds. #FormalMethods
• Some type constructors are tensor products. ~ Dan Piponi (sigfpe). #Haskell #FunctionalProgramming
• Tries for polynomials. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming #Math
• Emacs is my browser. ~ Joshua Blais. #Emacs
• Demostraciones con Lean 4 de "La sucesión 1, -1, 1, -1, … no es convergente". #LeanProver #Math
• Las matemáticas en la era de la IA: de la escasez a la abundancia de demostraciones. #AI4Math