# Fresh from the Labs

Here's one for the mind-bending category. 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 program....Hilbert II wants to become a free, world-wide mathematical knowledge base that contains mathematical theorems 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 argumentation to a formal syntax. That means, whenever in mathematics a certain kind of argumentation 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 mathematician to put theorems and proofs into that knowledge base. These proofs are automatically verified by a proof-checker. Also, texts in “common mathematical language” 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 centrally administrated and references to any location in the Internet are possible, a world-wide mathematical knowledge base could be built. Any proof of a theorem in this “mathematical web” could be drilled down to the very elementary rules and axioms. Think of an incredible number of mathematical textbooks 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.

**
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 prototype 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 inaccurate in the process of writing this section). 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.

Webstart Version: www.qedeq.org/0_03_10/webstart/qedeq.jnlp

QED Manifesto: ftp.mcs.anl.gov/pub/qed/manifesto

John Knight is the New Projects columnist for Linux Journal.

## Trending Topics

## Webinar

### Practical Task Scheduling Deployment

July 20, 2016 12:00 pm CDT

One of the best things about the UNIX environment (aside from being stable and efficient) is the vast array of software tools available to help you do your job. Traditionally, a UNIX tool does only one thing, but does that one thing very well. For example, grep is very easy to use and can search vast amounts of data quickly. The find tool can find a particular file or files based on all kinds of criteria. It's pretty easy to string these tools together to build even more powerful tools, such as a tool that finds all of the .log files in the /home directory and searches each one for a particular entry. This erector-set mentality allows UNIX system administrators to seem to always have the right tool for the job.

Cron traditionally has been considered another such a tool for job scheduling, but is it enough? This webinar considers that very question. The first part builds on a previous Geek Guide, Beyond Cron, and briefly describes how to know when it might be time to consider upgrading your job scheduling infrastructure. The second part presents an actual planning and implementation framework.

Join *Linux Journal*'s Mike Diehl and Pat Cameron of Help Systems.

Free to *Linux Journal* readers.

SUSE LLC's SUSE Manager | Jul 21, 2016 |

My +1 Sword of Productivity | Jul 20, 2016 |

Non-Linux FOSS: Caffeine! | Jul 19, 2016 |

Murat Yener and Onur Dundar's Expert Android Studio (Wrox) | Jul 18, 2016 |

Rogue Wave Software's Zend Server | Jul 14, 2016 |

Webinar: Practical Task Scheduling Deployment | Jul 14, 2016 |

- SourceClear Open
- SUSE LLC's SUSE Manager
- My +1 Sword of Productivity
- Tech Tip: Really Simple HTTP Server with Python
- Managing Linux Using Puppet
- Non-Linux FOSS: Caffeine!
- Doing for User Space What We Did for Kernel Space
- Murat Yener and Onur Dundar's Expert Android Studio (Wrox)
- Google's SwiftShader Released
- Parsing an RSS News Feed with a Bash Script

## Geek Guides

With all the industry talk about the benefits of Linux on Power and all the performance advantages offered by its open architecture, you may be considering a move in that direction. If you are thinking about analytics, big data and cloud computing, you would be right to evaluate Power. The idea of using commodity x86 hardware and replacing it every three years is an outdated cost model. It doesn’t consider the total cost of ownership, and it doesn’t consider the advantage of real processing power, high-availability and multithreading like a demon.

This ebook takes a look at some of the practical applications of the Linux on Power platform and ways you might bring all the performance power of this open architecture to bear for your organization. There are no smoke and mirrors here—just hard, cold, empirical evidence provided by independent sources. I also consider some innovative ways Linux on Power will be used in the future.

Get the Guide