Architecture of proof assistants

Have you ever wondered what mathematical proof assistant to use? Here
is a quick guide to their architectures.

HOL Light


HOL Light has an exquisite minimal design. It has the smallest kernel
of any system. John Harrison is the sole permanent occupant, but he
is very welcoming to guests.


tower-cranes-airport-istanbulLean is ambitious, and it will be massive. Do not be fooled by the name.
Construction area keep out” signs are prominently posted on the
perimeter fencing.


Moscow ministry of foreign affairsOnce the clear front-runner, it now shows signs of age. Do not expect
to understand the inner workings of this system unless you have been
trained in Warsaw.



Coq is built of modular components on a foundation of dependent type theory. This system has grown one PhD thesis at a time.


Is-Hearst-Tower_619X313Designed for use with multiple foundational architectures, Isabelle’s early
development featured classical constructions in set theory. However,
its largest modern tower is HOL.


Squatters in Venezuela

Does this really work? Defying expectations, Metamath seems to function
shockingly well for those who are happy to live without plumbing.


Formal Abstracts – a Vision

The Formal Abstracts (FABSTRACTS) project will establish a formal abstract service that will express the results of mathematical publications in a computer-readable form that captures the semantic content of publications.

Specifically, the service will

  • give a statement of the main theorem of each published mathematical paper in a language that is both human and machine readable.
  • link each term in theorem statements to a precise definition of that term (again in human/machine readable form), and
  • ground every statement and definition in the system in some foundational system for doing mathematics (the Lean theorem prover).

What is the long-term vision for Formal Abstracts (FABSTRACTS) in mathematics?

FABSTRACTS enables machine learning in math

Many mathematicians dream that computers will someday fundamentally
transform how mathematics is practiced, and FABSTRACTS expresses
in concrete terms how that transformation might be achieved.

Automation of mathematics has been a major aim of artificial
intelligence from its inception. This broad aim includes all aspects
of mathematical activity such as conjecturing, generating examples,
finding counterexamples, computing, learning,
collaborating, proving, generalizing, refereeing and checking,
searching, exploring, and transforming the literature.

For many of these activities, it is important or even essential to
have a machine-readable semantic representation of mathematical
objects. This is achieved by FABSTRACTS.

We foresee tools for exploration such as a Google Earth for
mathematics, providing an intuitive visual map of the entire world of
mathematics, combining formal abstracts, computation, and other
networked content — all displayed at user-selected resolution.

It gets easier

Just as the FABSTRACTS project will enable AI in mathematics, the
development of AI will enable FABSTRACTS.

Looking forward beyond the challenging initial groundwork to get
FABSTRACTS up and running, the generation of formal abstracts will
become nearly fully automated. The production of formal abstracts
will become easier and more efficient with every passing year.

Tools for the natural language processing of mathematics are under
development. As these tools develop, automation will replace the
manual preparation of formal abstracts. Automation will make it feasible
to construct hundreds of thousands (and eventually millions)
of formal abstracts.

For example, Kofler and Neumaier have developed a powerful parser for common mathematical language, and Neumaier is currently rewriting some of his
published math books in multilingual editions so as to be parsed and
translated by their software.  In other promising work,
Ganesalingam’s thesis gave a brilliant linguistic analysis of the
language of mathematics. The current Naproche (Natural language
Proof Checking) system accepts a rich subset of mathematical language
including TeX-style formulas.

We expect mathematicians to be able to supply their own formal abstracts
in a structured English format, which will be parsed and translated to the Lean language.

We foresee future cooperation between FABSTRACTS and a major math
abstract service (such as zbMATH or MathSciNet).
The abstract service will provide statements of
theorems from publications in a form suited for fast formal
abstraction, and with FABSTRACTS offering enhancements to those services.

Progress in document analysis will eventually permit the automated
extraction of formal abstracts directly from the documents (building
on the work of M. Suzuki and collaborators at Kyushu University).

FABSTRACTS as a permanent service

FABSTRACTS will become integrated with the workflow of
several tens of thousands of mathematicians.

We foresee a TeX package that allows mathematicians to cite formal
definitions and theorem statements for the convenience of readers, and
for the automatic processing of texts:

Let $M$ be a \formal{banach manifold}[]. %TeX

We foresee further integration of FABSTRACTS with computation (in the
style of the current SageTeX package, which performs SageMath
computation and graphics from within a TeX document).

We foresee the translation of formal abstracts into many languages
and formats. Lewis has constructed a two-way bridge between Mathematica and Lean. Computer programs already exist that give automated translations between some of the major proof assistants. The work of Kohlhase, Rabe, and
their coworkers develops general infrastructure for the translation of
formal mathematics between different systems. The point is
that before we translate, we first need any formal representation,
and that is achieved by FABSTRACTS.

There are many expected applications,
including training sets for machine learning, enhancement of automated
theorem proving technologies, machine translation of mathematical
texts into foreign languages, detecting errors in the mathematical
literature, and intelligent mathematical search

Finally, we foresee that FABSTRACTS will inspire a broader movement
for the increased precision in science, with mathematicians taking up
the challenge to formalize the proofs of formal abstracts, and
scientists finding precise ways to give formal expression to the
objects of their research.

Formal Abstracts in Mathematics

The Sloan Foundation has announced funding for a project to develop Formal Abstracts in Mathematics (FABSTRACTS).


To develop software and services for transforming mathematical results as they appear in journal article abstracts into formally structured data that machines can read, process, search, check, compute with, and learn from as logical statements.


  1. Careful and curated capture of at least 5,000 formal definitions and 2,000 formal abstracts of theorems.
  2. A “training set” that allows for Machine Learning and other automation techniques to improve the efficiency in capturing formal abstracts by at least 30%.
  3. A functional service for mathematicians to search and contribute formal abstracts.
  4. Wide adoption of the service as measured by thousands of unique uses of the service in the first six months it is available.