A Certifying Proof Assistant for Synthetic Mathematics in Lean
summary
SynthLean embeds a deep embedding of Martin-Löf type theory as a DSL inside Lean and implements certifying normalization-by-evaluation typechecking that emits Lean proof terms the kernel verifies. The project formalizes syntax (universes, Π, Σ, identity types, axiomatized constants), formalizes natural model semantics and proves soundness, and ships a workflow where constructions live either internally in MLTT or externally in semantic models; inductive/HITs are not yet supported but artifacts and code are available.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:21Synthetic mathematics
- 3:14Synthetic vs analytic math
- 5:21Goals of the assistant
- 7:29Syntax of type theory
- 9:58Categorical semantics
- 12:05Implementation
- 16:41Challenges in formalization
- 17:22Future directions
- 17:44Q&A
related talks
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future
10mWhen Does a Program Typecheck?
22mTowards Automated Verification of LLM-Synthesized C Programs
38mAutomatically Synthesising Programs that We Can Trust
12mLanguage-Model Probabilistic Programming for Improving Autoformalization via Cycle(…)
26m(...) How to turn (Liquid) Haskell into a theorem prover
19mVelvet: A Multi-Modal Verifier for Effectful Programs
01h 04mThe Leibniz Library and Applied Propositions as Types