Anatomy of a Formal Proof
Jeremy Avigad, Johan Commelin, Heather Macbeth, Adam Topaz
TL;DR
The experience of working with a proof assistant is described and the impact the technology will have on mathematics is considered.
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.