constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
A project bringing formal proof and proof assistants (particularly Lean) into the practice of undergraduate mathematics.
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
based on cubical type theory:
based on modal type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq and Agda)
Xena project (using Lean)
Other proof assistants
Historical projects that died out:
Kevin Buzzard, Using Lean with undergraduate mathematicians, talk at Lean Together 2019 (recording)
Kevin Buzzard, The future of Mathematics?, public lecture at the 80th anniversary celebration of CNRS, May 2019 (recording)
Last revised on September 12, 2019 at 07:06:25. See the history of this page for a list of all contributions to it.