Return to Answer

There are two threads of current development in proof systems: foundational and coverage. The foundational work tries to find the best meta-theory to formalize mathematics. Out of that work first came dependent types (AUTOMATH, in the late 60s), then the Calculus of Constructions (early Coq), and the Calculus of Inductive Constructions (current Coq). Currently a new wave of such work is being done in homotopy type theory as another step in this direction. Coq's library is not that large, except of course in the area of group theory where the results of the work on Feit-Thompson has produce something larger.

The much larger work has happened for decades building Mizar's enormous library [Note that Mizar is based on Tarski-Grothendieck set theory rather than type theory. Its library is a couple of orders of magnitude larger than anyone else's. Also worth a close look is NuPRL, HOL light and Isabelle, which all have decently sized libraries.

A rather thorough list of math systems has been collected by Freek Wiedijk.

Personally, I must admit that for the sheer joy of playing with mathematics, I rather like to use Agda. Unfortunately, its current library is fairly small, but the community is growing it quite quickly. For developing the kinds of mathematics I am currently interested in, it works quite well.

This whole area is the domain currently called mechanized mathematics -- there is an annual conference on that topic, with this (2013) year's instalment happening in early July in Bath.

Bottom line: none of these pieces of software are at the level of ease-of-use of say Maple or Mathematica, although some of them are probably close to SAGE. But they are evolving very quickly. They are way past the innovator stage, firmly into early adopter territory and growing.

There are two threads of current development in proof systems: foundational and coverage. The foundational work tries to find the best meta-theory to formalize mathematics. Out of that work first came dependent types (AUTOMATH, in the late 60s), then the Calculus of Constructions (early Coq), and the Calculus of Inductive Constructions (current Coq). Currently a new wave of such work is being done in homotopy type theory as another step in this direction. Coq's library is not that large, except of course in the area of group theory where the results of the work on Feit-Thompson has produce something larger.

The much larger work has happened for decades building Mizar's enormous library [Note that Mizar is based on Tarski-Grothendieck set theory rather than type theory. Its library is a couple of orders of magnitude larger than anyone else's. Also worth a close look is NuPRL, HOL light and Isabelle, which all have decently sized libraries.

A rather thorough list of math systems has been collected by Freek Wiedijk.

Personally, I must admit that for the sheer joy of playing with mathematics, I rather like to use Agda. Unfortunately, its current library is fairly small, but the community is growing it quite quickly. For developing the kinds of mathematics I am currently interested in, it works quite well.

This whole area is the domain currently called mechanized mathematics -- there is an annual conference on that topic, with this (2013) year's instalment happening in early July in Bath.

Bottom line: none of these pieces of software are at the level of ease-of-use of say Maple or Mathematica, although some of them are probably close to SAGE. But they are evolving very quickly. They are way past the innovator stage, firmly into early adopter territory and growing.

There are two threads of current development in proof systems: foundational and coverage. The foundational work tries to find the best meta-theory to formalize mathematics. Out of that work first came dependent types (AUTOMATH, in the late 60s), then the Calculus of Constructions (early Coq), and the Calculus of Inductive Constructions (current Coq). Currently a new wave of such work is being done in homotopy type theory as another step in this direction. Coq's library is not that large, except of course in the area of group theory where the results of the work on Feit-Thompson has produce something larger.

The much larger work has happened for decades building Mizar's enormous library [Note that Mizar is based on Tarski-Grothendieck set theory rather than type theory. Its library is a couple of orders of magnitude larger than anyone else's. Also worth a close look is NuPRL, HOL light and Isabelle, which all have decently sized libraries.

A rather thorough list of math systems has been collected by Freek Wiedijk.

Personally, I must admit that for the sheer joy of playing with mathematics, I rather like to use Agda. Unfortunately, its current library is fairly small, but the community is growing it quite quickly. For developing the kinds of mathematics I am currently interested in, it works quite well.

This whole area is the domain currently called mechanized mathematics -- there is an annual conference on that topic, with this (2013) year's instalment happening in early July in Bath.

Bottom line: none of these pieces of software are at the level of ease-of-use of say Maple or Mathematica, although some of them are probably close to SAGE. But they are evolving very quickly. They are way past the innovator stage, firmly into early adopter territory and growing.

There are two threads of current development in proof systems: foundational and coverage. The foundational work tries to find the best meta-theory to formalize mathematics. Out of that work first came dependent types (AUTOMATH, in the late 60s), then the Calculus of Constructions (early Coq), and the Calculus of Inductive Constructions (current Coq). Currently a new wave of such work is being done in homotopy type theory as another step in this direction. Coq's library is not that large, except of course in the area of group theory where the results of the work on Feit-Thompson has produce something larger.

The much larger work has happened for decades building Mizar's enormous library [Note that Mizar is based on Tarski-Grothendieck set theory rather than type theory. Its library is a couple of orders of magnitude larger than anyone else's. Also worth a close look is NuPRL, HOL light and Isabelle, which all have decently sized libraries.

A rather thorough list of math systems has been collected by Freek Wiedijk.

Personally, I must admit that for the sheer joy of playing with mathematics, I rather like to use Agda. Unfortunately, its current library is fairly small, but the community is growing it quite quickly. For developing the kinds of mathematics I am currently interested in, it works quite well.

This whole area is the domain currently called mechanized mathematics -- there is an annual conference on that topic, with this (2013) year's instalment happening in early July in Bath.

Bottom line: none of these pieces of software are at the level of ease-of-use of say Maple or Mathematica, although some of them are probably close to SAGE. But they are evolving very quickly. They are way past the innovator stage, firmly into early adopter territory and growing.

There are two threads of current development in proof systems: foundational and coverage. The foundational work tries to find the best meta-theory to formalize mathematics. Out of that work first came dependent types (AUTOMATH, in the late 60s), then the Calculus of Constructions (early Coq), and the Calculus of Inductive Constructions (current Coq). Currently a new wave of such work is being done in homotopy type theory as another step in this direction. Coq's library is not that large, except of course in the area of group theory where the results of the work on Feit-Thompson has produce something larger.

The much larger work has happened for decades building Mizar's enormous library [Note that Mizar is based on Tarski-Grothendieck set theory rather than type theory. Its library is a couple of orders of magnitude larger than anyone else's. Also worth a close look is NuPRL, HOL light and Isabelle, which all have decently sized libraries.

A rather thorough list of math systems has been collected by Freek Wiedijk.

Personally, I must admit that for the sheer joy of playing with mathematics, I rather like to use Agda. Unfortunately, its current library is fairly small, but the community is growing it quite quickly. For developing the kinds of mathematics I am currently interested in, it works quite well.

This whole area is the domain currently called mechanized mathematics -- there is an annual conference on that topic, with this (2013) year's instalment happening in early July in Bath.

Bottom line: none of these pieces of software are at the level of ease-of-use of say Maple or Mathematica, although some of them are probably close to SAGE. But they are evolving very quickly. They are way past the innovator stage, firmly into early adopter territory and growing.

There are two threads of current development in proof systems: foundational and coverage. The foundational work tries to find the best meta-theory to formalize mathematics. Out of that work first came dependent types (AUTOMATH, in the late 60s), then the Calculus of Constructions (early Coq), and the Calculus of Inductive Constructions (current Coq). Currently a new wave of such work is being done in homotopy type theory as another step in this direction. Coq's library is not that large, except of course in the area of group theory where the results of the work on Feit-Thompson has produce something larger.

The much larger work has happened for decades building Mizar's enormous library [Note that Mizar is based on Tarski-Grothendieck set theory rather than type theory. Its library is a couple of orders of magnitude larger than anyone else's. Also worth a close look is NuPRL, HOL light and Isabelle, which all have decently sized libraries.

A rather thorough list of math systems has been collected by Freek Wiedijk.

Personally, I must admit that for the sheer joy of playing with mathematics, I rather like to use Agda. Unfortunately, its current library is fairly small, but the community is growing it quite quickly. For developing the kinds of mathematics I am currently interested in, it works quite well.

This whole area is the domain currently called mechanized mathematics -- there is an annual conference on that topic, with this (2013) year's instalment happening in early July in Bath.

Bottom line: none of these pieces of software are at the level of ease-of-use of say Maple or Mathematica, although some of them are probably close to SAGE. But they are evolving very quickly. They are way past the innovator stage, firmly into early adopter territory and growing.