The goal of Hilbert II, which is in the tradition of Hilbert's program, is the creation of a system that enables a working mathematician to put theorems and proofs (in the formal language of predicate calculus) into it. These proofs are automatically verified by a proof checker. Because this system is not centrally administered and enables references to any location on the Internet, a world wide mathematical knowledge base could be built. It also contains information in "common mathematical language".


This is a mongaga release. The application may now be run with Java Web Start. A preferences window was added and enables the user to view and edit some settings. The formula parser is also integrated and makes it possible to transform LaTeX formulas into QEDEQ formulas. The parser can be controlled by changing or adding operators to the XML file "mengenlehreMathOperators.xml" in the config directory.

URL: Hilbert II - Introduction