Anatomy of a Formal Proof

TL;DR

This paper discusses the use of interactive proof assistants in formalizing mathematical proofs, highlighting their potential impact on the practice and understanding of mathematics.

Contribution

It provides an analysis of working with proof assistants and explores their influence on mathematical methodology and rigor.

Findings

Proof assistants enable formal verification of mathematical proofs.

They have the potential to transform mathematical research and education.

The paper offers insights into the practical experience of using proof assistants.

Abstract

Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a computer can parse them and check them against the rules of a formal axiomatic foundation. This article describes the experience of working with a proof assistant and considers the impact the technology will have on mathematics.