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".

Changes

Now QEDEQ modules may be removed within the GUI, and all dependent modules will change their state accordingly. Within the LaTeX parts, the new command "\qref" is supported. It references to a Node from the local or an imported QEDEQ module. UTF-8 and ISO-8859-1 are now correctly parsed, and error lines are translated accordingly. The mathematical XML files have fewer errors and contain more (still informal, but very close to formal) proofs. Under the hood, a lot of refactoring took place.

URL: Hilbert II - Introduction