In one line, the motivation behind Ghilbert is:
There is value in humans interacting directly with formal proofs.
In this page, I’ll unpack this motto and describe how I hope Ghilbert will fulfill it. Ghilbert also strives to be:
☞ The Development of Proof Theory at the Stanford Encyclopedia of Philosophy. Most mathematicians work in informal proofs, natural language texts which persuade other mathematicians of the correctness of their arguments. Routine details are omitted, with the expectation that the reader could readily fill them in. By contrast, in a formal proof, all steps are explicit, and all terms are written out in full. The common notation “...” is not generally allowed in formal proofs.
☞ Hilbert system at Wikipedia. As might be guessed from the name, Ghilbert is based on Hilbert style formal proofs. A Hilbert style proof is basically a sequence of terms, each of which is an instance of an axiom or is derived from previous terms by an inference rule.
It’s commonly believed that formal proofs, particularly Hilbert style, are by their nature long, tedious and repetitious, and thus not conducive for humans to work with directly. Proof systems differ widely in how they deal with this. An extremely common approach is to automate the tedious and repetitious parts. Automation makes sense, but comes at a cost; automated theorem proving systems are dramatically more complex than simple proof checkers. Proof scripts which direct the automation generally require a programming language and are difficult to understand (especially for newcomers). This approach, while powerful, does not fulfill the goal of working directly with formal proofs.
☞ Metamath. Experience with the Metamath system shows another way. A major reason why proofs are long and tedious is that they contain repetitive sections, the same sequence of steps but with minor variations. In Metamath, these would be split out into derived rules, which are very similar to subroutine calls or macro expansions. Similarly, repetitive patterns in subterms can be split out into definitions. Perhaps surprisingly, deft use of these techniques has resulted in a large body of impressive theorems with reasonably short proofs, all of which were basically written by hand. Ghilbert adopts the Metamath style.
A major goal is for Ghilbert to be simple and easy to understand. Thus, it strips away all the non-essentials. In particular, Ghilbert is not a programming language (Coq, Lean, Agda, Idris), nor is it based on a programming language (as HOL implementations are based on ML).
The scope of Ghilbert is limited to proof checking rather than automated theorem proving. It is similar in this way to Metamath and Automath.
Because of the simplicity and limited scope, it should be practical to develop an ecosystem of tools around Ghilbert, including translations between other proof formats, automated proof search, and more. An encouraging sign is the dozen or so independent implementations of Metamath.
What is the most suitable axiomatic basis for mathematics? This is a deeply philosophical question, and it seems to me there is no definitive answer. Many proof systems (Mizar, Coq, HOL) pick a set of axioms that seem suitable. Other systems (Automath, Logical Framework, Isabelle, Metamath) are designed to work in a number of different logics. Ghilbert follows the latter approach.
I’d like to explore going a bit further, to encourage people to write proofs relying on the least set of axioms needed, then interpret these proofs so they’re still usable in more powerful axiomatic systems. This is similar to the Little Theories project of William Farmer et al.
Ideally, I’d like to split up the proof repository into modules where each module uses just the axioms and constructions it needs. This is a much more speculative aspect of the Ghilbert plan; it still feels worthwhile even if it ends up as a big monolithic structure like Metamath’s set.mm.
I’ve been tinkering with protoypes for Ghilbert for over a decade. Looking back, I think there are some good ideas, but also some mistakes.
I write this at the beginning of a 3 month retreat at the Recurse Center, where I hope to do a new implementation. I want to accomplish:
I’m interested in working with others on these pieces, as well as encouraging people to write and upload proofs to the repository.
Raph Levien • Recurse Center, New York City • 2017-08-15