\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

On Theorem Provers

Table of Contents

1. Introduction

There is much to say, too much. In the golden age of GOFAI, theorem provers were considered an integral component to an agent's reasoning capabilities. Needless to say, it didn't pan out, for AI. But in mathematics, there is much use for theorem provers as a way to formalize mathematics.

1.1. Components of a Theorem Prover

Basically a theorem prover is an interpreter for a foundations of mathematics. Andrej Bauer argues the basic structure could be described as several languages working together in concert:

Kernel
Validates every inference step and makes sure that proofs are correct, by implementing a formal system F sufficiently expressive allowing the formalization of a large body of math, sufficiently simple for an efficient implementation.
Vernacular
The input language the user writes a proof in, which is typically complex and accomodates notational conventions.
Elaborator
Translates the vernacular into the kernel's formal system.
Meta-Language
Quite literally the programming language used to implement the kernel and elaborator.

1.2. Vernacular

The design of the vernacular is quite difficult and under-studied. One possible dichotomy is between a Declarative style and a Procedural style. The former resembles how mathematicians actually reason, the latter resembles how the kernel actually works.

We can combine these two together, as evidenced by Wiedijk's work (arXiv:1201.3601).

Mizar's grammar is worth a case study in structuring a vernacular.

2. Rapid Prototyping

We can implement theorem provers quickly in functional languages. Indeed, ML was invented specifically to implement the LCF theorem prover. The use of algebraic data types was to implement the AST of formulas and logical languages, etc.

We can use Lisp (e.g., LaTTe).

2.1. Formalizing Mathematics

Actually, this is one of the least appreciated aspects of theorem provers: that we're trying to invent a formal language for doing mathematics. Instead, we end up with contrived proof formats and the proof assistant communities are so insular they don't realize how terrible it is.

What should be done instead is something like a "stepping stone" to theorem provers by using a "structured subset" of English. We need to identify the "subdomains" of mathematical practice, viz:

  • Formulating definitions
  • Stating theorems
  • Writing proofs

As far as formulating definitions, although I'm a partisan for Baez–Dolan "Stuff, Structure, Properties" (briefly discussed with Internalization), there are times when it's clunky (in topology, field theory and I suspect Galois theory). It may be useful to carve out the notion of adjectives (e.g., 'we call a function "continuous" if <property>'). At this point, it feels quite a bit like Mizar's approach to definitions. For more on this, see:

  • Josef Urban,
    "Translating Mizar for First Order Theorem Provers".
    In Mathematical Knowledge Management: Proceedings of the Second International Conference (Eds., A. Asperti, B. Buchberger, J.H. Davenport), Springer-Verlag, Lecture Notes in Computer Science vol 2594, 2003, pp. 203–215.

Stating theorems and proving them are rather tightly coupled. We could try formalizing a basic Mathematical Vernacular, similar to Wiedijk's variant of de Bruijn. This would give us proof steps, while leaving "stating theorems" completely unspecified.

The main point I'd like to drive home, however: it is wrong to just shrug and accept unintelligible commands as "the only way" to do theorem proving. Our goal is not to update Russell and Whitehead's Principia replacing archaic symbols with archaic keywords, nor should it be. Sadly this is what procedural provers have become (looking at you, Lean community).

3. References

  • John Harrison, Josef Urban and Freek Wiedijk,
    "History of Interactive Theorem Proving".
    PDF, 85 pages.
  • Jeremy Avigad,
    "The design of mathematical language".
    PDF, dated 29 Aug 2021, 35 pages (paper corresponding to a talk)

3.1. Vernacular

  • John Harrison,
    "A Mizar Mode for HOL".
    Eprint, 19 pages.
  • John Harrison,
    "Proof Style".
    Eprint, 19 pages.
  • Freek Wiedijk,
    "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving".
    Eprint: arXiv:1201.3601, 26 pages.

3.1.1. Mizar

  • Andrzej Trybulec,
    "Some Features of the Mizar Language".
    Eprint, 1993, 17 pages.
  • Josef Urban,
    "Translating Mizar for First Order Theorem Provers".
    In Mathematical Knowledge Management: Proceedings of the Second International Conference (Eds., A. Asperti, B. Buchberger, J.H. Davenport), Springer-Verlag, Lecture Notes in Computer Science vol 2594, 2003, pp. 203–215.

3.2. Mathematical Analysis in Theorem Provers

  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond,
    "Formalization of Real Analysis: A Survey of Proof Assistants and Libraries".
    PDF, 40 pages.
  • Micaela Mayero,
    "Using theorem proving for numerical analysis: Correctness proof of an automatic differentiation algorithm".
    In TPHOLs 2002: Theorem Proving in Higher Order Logics, pp 246–262.

Last Updated 2021-11-22 Mon 15:33.