Hilbert is back..

We are in the tradition of Hilbert's program and present a new
software version of *Hilbert II*. The goal of *Hilbert II* is free
access to verified and readable mathematical knowledge. The
mathematical texts are more than ordinary text books because they also
contain formal proofs. The project is still in development but there
is exists a working prototype that can verify formal proofs and the
main program suite can already do some syntactical checks for new
QEDEQ modules. We even produced a script about axiomatic set theory
(Morse-Kelley) in LaTeX form out of such a module. All this can be
done with a quite nice GUI...

For more details look under:
http://www.qedeq.org/

You can simply check out the new version by clicking on the Java Web
Start link http://www.qedeq.org/current/webstart/qedeq.jnlp

.