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".
METAGRAF is a graphical editor for creating figures in MetaPost. It is currently able to draw any kind of figure in b/w or color. METAGRAF outputs a MetaPost file which can then be run through MetaPost by itself or using TeX. The program is written in Java and is thus platform-independent.