Specifications

Hilbert II
Here’s one for the mind-bending cate-
gory. In this age of shared information
and decentralization comes another
cool addition to the realm of shared
consciousness. Hilbert II attempts to
resurrect and build on the ideals of a
near-dead project, QED (check the link
at the end for a copy of QED’s manifesto).
Hilbert II’s goals are:
...decentralised access to verified
and readable mathematical
knowledge. As its name already
suggests, this project is in the
tradition of Hilbert’s pro-
gram....Hilbert II wants to
become a free, world-wide
mathematical knowledge base
that contains mathematical the-
orems and proofs in a formal
correct form. All belonging
documents are published under
the GNU Free Documentation
License. We aim to adapt the
common mathematical argu-
mentation to a formal syntax.
That means, whenever in mathe-
matics a certain kind of argu-
mentation is often used, we will
look forward to integrate it into
the formal language of Hilbert II.
This formal language is called
the QEDEQ format.
Hilbert II provides a program
suite that enables a mathemati-
cian to put theorems and proofs
into that knowledge base. These
proofs are automatically verified
by a proof-checker. Also, texts in
“common mathematical lan-
guage” can be integrated. The
mathematical axioms, definitions
and propositions are combined
to so-called QEDEQ modules.
Such a module could be seen as
a mathematical textbook that
includes formal correct proofs.
Because this system is not cen-
trally administrated and refer-
ences to any location in the
Internet are possible, a world-
wide mathematical knowledge
base could be built. Any proof
of a theorem in this “mathemat-
ical web” could be drilled down
to the very elementary rules and
axioms. Think of an incredible
number of mathematical text-
books with hyperlinks, and each
of its proofs could be verified by
Hilbert II. For each theorem, the
dependency of other theorems,
definitions and axioms could be
easily derived.
The Complex World of Mathematical
Collaboration through Hilbert II
Installation First things first, Hilbert
II is a Java-based program. We generally
try to avoid Java-based projects because
this is Linux Journal, not “Platform-
Neutral Java Webstart Journal”, but
the cooler projects are definitely worth
examining, and besides, it does have a
Linux-specific version. For the lazy,
there is a webstart version that can be
launched from your browser (see the
link at the end of this section), which
requires you to have the Java browser
plugins installed. For the Linux version,
the precondition for a working proto-
type is a Java Runtime Environment, at
least version 1.4. Hilbert II uses LaTeX
for a lot of its functions, and there are
some potential bugs that frequent
users may run into, so check the Web
site for further information on possible
LaTeX requirements.
Head to the Download section of
the Web site and download the Linux
tarball. Extract it to your directory of
choice, and open a terminal in the new
qedeq directory.
At the console, enter:
$ ./qedeq_se.sh
Or, if that doesn’t work, enter:
$ sh qedeq_se.sh
Usage Hilbert II works around XML
files, and you’ll need some of these
XML files to get started. If you choose
File→Load from web, a default file is
provided from which you can begin to
experiment. If you look in the main
window, there’s a tab called QEDEQ.
Clicking on any entry on the left
displays its nuts and bolts in this tab.
Under Tools→LaTeX to QEDEQ, you
can start playing around with your own
formulae, and under Check→Check
Mathematical Logic, you can make sure
that your syntax and so on check out.
To export your work for the world to
see, going to Transform→Create LaTeX
output creates a new LaTeX .tex file in
the generated folder under qedeq.
But from here, you’re on your own,
because I haven’t got a clue what I’m
talking about in this world of advanced
mathematics and formulae (and I’ve
probably said something wildly inaccu-
rate in the process of writing this sec-
tion). However, I’m keen to see the
results of this academic collaboration,
where ideally knowledge should keep
advancing and continue to be built upon,
and I hope to see more of these mind-
bending shared-consciousness projects.
I Webstart Version: www.qedeq.org/
0_03_10/webstart/qedeq.jnlp
I QED Manifesto: ftp.mcs.anl.gov/
pub/qed/manifesto
vitetris
Ever been stuck working on a text-only
mailing server and wished you had
38 | august 2008 www.linuxjournal.com
NEW PROJECTS
Fresh from the Labs
(www.qedeq.org)
(victornils.net/tetris)