Proof Assistants for PL and Math
summary
Panel reports active, practical work: large libraries (Lean + mathlib, ~700k LOC) and successful formalizations (including the four‑color style project and deep algebraic definitions like perfectoid spaces) exist and scale unevenly; cubical/type‑theory extensions try to fix quotients/canonicity problems but complicate evaluation; automation via SMT/Z3 and verified tactics (proof‑by‑reflection, metacoq style) is the proposed path to keep proof objects small and checkable; engineering issues—porting Lean3→4, search across heterogeneous libraries, and proof certificate formats for composition—decide whether this work helps your needs.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:54Kevin Buzzard
- 6:13What I Learned from Building those Proof of System
- 9:07How Do We Define Such Certified Api
- 13:42Scalability
- 17:05What Are the Most Important Differences between How Proof Assistance Should Be Used in Programming Languages versus Math
- 25:58Promising Directions for Encoding Algebraic Hierarchies
- 55:28What Are Everyone's Top Recommendations for Improving Education and or Outreach To Get More People Using Proof Assistance
- 57:52Usability Issues in Proof of Systems