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:

- Simple and easy to understand
- Agile with respect to choice of axiomatization
- Interoperable with other tools

☞
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:

- Redesigning the proof language
- Reimplementing the command line verifier (in Rust)
- Doing an editor plugin (for xi-editor) to help write proofs
- Building a static webpage generator to create pages like Metamath's proof explorer
- Writing a translator for Metamath’s set.mm into Ghilbert

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