Formal Abstracts

About the project

The Formal Abstracts project was initiated by Thomas Hales in 2017. See his talk Big conjectures from the Big Proof meeting in Cambridge.

A formal abstract, or fabstract for short, is a formalization of the main results (constructions, definitions, proofs, conjectures) of a piece of informal mathematics, such as a research paper. There is no requirement that the entire text be formalized. Proofs of statements are omitted. A formal abstract is not the formalization of the abstract itself.

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 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.

For more information about the goals of the project, see Hales’ blog posts here and here.

Project status

We are currently in a design phase. The GitHub repository contains experiments, but these do not necessarily reflect the future direction of the project. Current projects include the development of a base library in Lean and infrastructure around this library.

We are not actively seeking contributions at this time.