Anatomy of a Formal Proof
History and Overview
2024-11-20 v1 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.2411.11885,
title = {Anatomy of a Formal Proof},
author = {Jeremy Avigad and Johan Commelin and Heather Macbeth and Adam Topaz},
journal= {arXiv preprint arXiv:2411.11885},
year = {2024}
}
Comments
12 pages