nLab MathScheme



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
completely presented setdiscrete object/0-truncated objecth-level 2-type/set/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels



Constructivism, Realizability, Computability



MathScheme is a project aimed at combining computation via computer algebra? with formal proof via proof assistants.

From their Mission page:

Sound mathematics is essential in all modern technological developments. As we build increasingly complex systems, mathematical reasoning becomes more difficult and error-prone. This is particularly true for software systems. A mechanized mathematics system (MMS) is required that can support, improve, and — where possible — automate mathematical reasoning.

There are presently two major types of MMSs, computer algebra systems and computer theorem proving systems. Computer algebra systems provide algorithms for symbolic computation. They are relatively fast and easy to use, but they are not rigorously based, untrustworthy, and narrow in scope. Computer theorem proving systems provide tools for creating formal proofs. They are based on well-defined logical foundations, can support a wide range of mathematics, but are difficult to use and often lack the specific knowledge needed to perform many routine computations.

While mechanized mathematics has the potential to revolutionize the design, implementation, and analysis of software systems, contemporary MMSs fall well short of this potential. There are no MMSs today that provide highly integrated symbolic computation and formal deduction capabilities. There have been earlier attempts to add the capabilities of one type of MMS to an existing system of the other type or to combine two existing systems of different type, but these attempts have not been very successful. One cannot add fundamental capabilities as an afterthought.

Our objective is to develop a new approach to mechanized mathematics that combines the strengths of symbolic algebra systems with those of formal deduction systems to yield a system that is both powerful and sound. The first goal of the project is to develop a formal framework that integrates symbolic computation and formal deduction. The framework should allow mathematical knowledge to be represented both declaratively using axioms and procedurally using algorithms, and it should provide a style of mathematical reasoning in which computation and deduction are intertwined.

The second project goal is to design and implement an MMS based on the formal framework. It should provide services for building formal languages, theories, computations, deductions, and mappings between theories — the services that are necessary for mechanizing the mathematics process.

Our long-range goal is to build, on top of the MMS, an interactive mathematics laboratory (IML) that provides an integrated set of tools for facilitating and managing mathematical reasoning. The IML is intended to have the capabilities of both contemporary computer algebra systems and computer theorem proving systems and the means to formalize a wide range of mathematical knowledge.

proof assistants:

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:

For higher category theory:

projects for formalization of mathematics with proof assistants:

Other proof assistants

Historical projects that died out:


Last revised on September 12, 2019 at 03:07:26. See the history of this page for a list of all contributions to it.