lean 2 Type Theory Part III: Verifying Formal Specifications Nov 5, 2025 Type Theory Part II: Proving Natural Addition Commutes from First Principles Sep 20, 2025