UP
formal maths net links

qed The ANL QED Home Page Manifesto QED94 Workshop
The Stanford QED Page Archive QED95 Workshop
ANL ftp site Holmes on metalogic and QED stuff
Dan Connolly's QED survey.
mechanisation of mathematics
AUTOMATH
Semantics
Selected Papers
a proof
automation of reasoning
Mizar The Journal of
Formalised Mathematics
jrh Formalised
Mathematics
Logiweb Logiweb is a system for creating a world wide web of theorems, proofs, and much more.
MetaMath a detailed formal derivation by Norman Megill of real and complex arithmetic from something like Zermelo Fraenkel set theory.
Harvey M. Friedman on The Formalisation of Mathematics (postscript)
DReaM - Discovery and Reasoning in Mathematics
Omega - a mixed-initiative system with the ultimate purpose of supporting theorem proving in main-stream mathematics and mathematics education. It has a distributed web architecture which integrates a number of mathematical services. Currently these services are a proof planner, a collection of tools for formulating problems, for proving subproblems, and proof presentation.
CALCULEMUS - Systems for Integrated Computation and Deduction
Theorem Proving with the Real Numbers - John Harrison's Doctoral Thesis
The 4-colour theorem in Coq - by Georges Gonthier
Formalising 100 Theorems - by Freek Wiedijk
The Flyspeck Project - a project formalising the proof of the Kepler Conjecture by Thomas Hales

Mailing List

qed
Mailing list for those interested in QED, an ambitious project to mechanise mathematics. Messages to qed@mcs.anl.gov, subscription requests to qed-request. The mailing list is maintained automatically by majordomo@mcs.anl.gov
The material linked to from this page is about automating mathematics by formal proof (together with references to pages for automating mathematics and and proof separately). In some cases, technology intended for just one of these areas may nevertheless be suitable for the combination.

Mizar and Automath are both systems which have been used extensively for developing machine checked formal proofs in a variety of branches of mathematics.

The QED project is as yet more aspiration than reality. The aspiration includes the computerised formalisation of substantial parts of mathematics.

All of these projects seem to be concerned primarily with the development rather than the application of mathematics, where proof is traditionally thought most relevant. The possibility of using logic for problem solving in applied mathematics has so far attracted little interest.

UP HOME © RBJ created 1995/10/8 modified 2009/8/13