Readings shared March 29, 2026
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