-*- outline -*-

* proofgeneral.

  $ sudo apt-get install proofgeneral

  $ sudo apt-get install proofgeneral-coq

  $ sudo apt-get install proofgeneral-misc

  $ sudo apt-get install proofgeneral-doc

  $ sudo apt-get install proofgeneral-minlog

or build from source:

  $ make clean

  $ make compile EMACS=xemacs

  $ cat ~/.emacs

...

(load-file "dir/generic/proof-site.el")

...

See

  http://proofgeneral.inf.ed.ac.uk/

* Isabelle.

Isabelle is a generic proof assistant.

It allows mathematical formulas to be expressed in a formal language and

provides tools for proving those formulas in a logical calculus. The main

application is the formalization of mathematical proofs and in particular

formal verification, which includes proving the correctness of computer

hardware or software and proving properties of computer languages and

protocols.

See

  http://isabelle.in.tum.de/overview.html

  http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)

* IsarMathLib.

The goal of the project is to create a library of formalized mathematics,

similar to the Mizar Mathematical Library, but written for the Isabelle/Isar

theorem prover (ZF logic).

See

  http://savannah.nongnu.org/projects/isarmathlib

  http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel

** http://isarmathlib.org/

This site is an experimental HTML rendering of fragments of the IsarMathLib

project. IsarMathLib is a library of mathematical proofs formally verified by

the Isabelle theorem proving environment. The formalization is based on the

Zermelo-Fraenkel set theory.

** Tiddly Formal Math.

This site is an experimental TiddlyWiki rendering of fragments of the

IsarMathLib project. IsarMathLib is a library of mathematical proofs formally

verified by the Isabelle theorem proving environment. The formalization is

based on the Zermelo-Fraenkel set theory.

See

  http://formalmath.tiddlyspot.com/