The readings shared in Bluesky on 29 March 2026 are:

• Embracing AI and formalization: Experimenting with tomorrow’s mathematical tools. ~ Jarod Alper. #AI4Math #LeanProver #ITP #Math
• On the paucity of lattice triangles. ~ David Kurniadi Angdinata, Evan Chen, Ken Ono, Jiaxin Zhang, Jujian Zhang. #LeanProver #ITP #Math
• Executable Gödel encodings: A verified runtime for logical syntax. ~ Adrian Diamond. #LeanProver #ITP #Logic #Math
• Lean: Collaboration using formalization. ~ Floris van Doorn. #LeanProver #ITP #Math
• Formalizing the sphere packing problem. ~ Maryna Viazovska. #LeanProver #ITP #Math
• A Lean formalisation of sphere packing in dimension 8. ~ Siddharth Hariharan. #LeanProver #ITP #Math
• Autoformalization: A year of progress. ~ Auguste Poiroux. #AI4Math #LeanProver
• Videos of talks at Swiss Mathematical Society Spring Meeting "Formalization and Proof Assistants" at UniDistance Suisse, 27/03/2026. #LeanProver
• Formally verifying digital circuits with category theory in Lean. ~ Matt Hunzinger. #LeanProver #ITP #CategoryTheory
• Shaping the future of mathematics in the age of AI. ~ Johan Commelin, Mateja Jamnik, Rodrigo Ochigame, Lenny Taelman, Akshay Venkatesh. #AI4Math #LeanProver #ITP
• What happens when AI starts checking mathematicians’ work. ~ Manon Bischoff. #AI4Math #LeanProver
• As AI keeps improving, mathematicians struggle to foretell their own future. ~ Joseph Howlett. #AI4Math #LeanProver
• Mathematics in the library of Babel. ~ Daniel Litt. #AI4Math
• Claude, mon ami (Eine intellektuelle romanze). ~ Martin Burckhardt. #AI #Programming