Proof Assistants

concepts · 2 notes linked

Related: Michael Shulman · Homotopy Type Theory · Category Theory · Type Theory · Kevin Buzzard · Lean Prover · Imperial College London · Formal Verification

Notes

• Formalising mathematics - an introduction — Kevin Buzzard on Lean proof assistant and digitizing mathematics
• Michael Shulman: Papers — Michael Shulman's research index on category theory and homotopy type theory