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
basic constructions:
strong axioms
further
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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.
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
based on cubical type theory:
1lab (cross-linked reference resource)
based on modal type theory:
based on simplicial 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:
Last revised on September 12, 2019 at 07:07:26. See the history of this page for a list of all contributions to it.