As these papers show, the state of the art is still extremely primitive from an user-friendliness point of view. Formalized math proofs still read too little like math and too much like computer code.
The issue is exacerbated since most proof assistants in common use today are “procedural” proof assistants. A proof in a procedural proof assistant is a linear list of complex proof “tactics” which involve manipulation of the proof state: hypotheses and goals are typically left implicit. These scripts are unreadable unless one replays them step-by-step in the proof assistant.
The most interesting project seems to be http://www.vdash.org—which is intended to be a formal math wiki. The website features a lot of background information but the wiki itself is not up and running, and discussions in the mailing list seem to have died off.
Another useful site is http://www.formalmath.org : it is a “user-friendly” presentation of IsarMathLib, a library for the Isabelle proof assistant based on Zermelo-Frankel set theory.
The December 2008 issue of AMS Notices is entirely devoted to formal proof: http://www.ams.org/notices/200811/
As these papers show, the state of the art is still extremely primitive from an user-friendliness point of view. Formalized math proofs still read too little like math and too much like computer code.
The issue is exacerbated since most proof assistants in common use today are “procedural” proof assistants. A proof in a procedural proof assistant is a linear list of complex proof “tactics” which involve manipulation of the proof state: hypotheses and goals are typically left implicit. These scripts are unreadable unless one replays them step-by-step in the proof assistant.
The most interesting project seems to be http://www.vdash.org—which is intended to be a formal math wiki. The website features a lot of background information but the wiki itself is not up and running, and discussions in the mailing list seem to have died off.
Another useful site is http://www.formalmath.org : it is a “user-friendly” presentation of IsarMathLib, a library for the Isabelle proof assistant based on Zermelo-Frankel set theory.