Readings shared September 12, 2025
The readings shared in Bluesky on 12 September 2025 are
- Finiteness of symbolic derivatives in Lean. ~ Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, Gabriel Ebner. #ITP #LeanProver #Math
- Modeling and proving in computational type theory using the Rocq prover. ~ Gert Smolka. #ITP #Rocq
- MPCTT textbook project (Modeling and proving in computational type theory using the Rocq prover). ~ Gert Smolka. #ITP #Rocq
- Introducing Gauss, an agent for autoformalization. #AI #Autoformalization #ITP #LeanProver #Math