Anatomy of a Formal Proof
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915025920196608 |
|---|---|
| author | Avigad, Jeremy Commelin, Johan Macbeth, Heather Topaz, Adam |
| author_facet | Avigad, Jeremy Commelin, Johan Macbeth, Heather Topaz, Adam |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_11885 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Anatomy of a Formal Proof Avigad, Jeremy Commelin, Johan Macbeth, Heather Topaz, Adam History and Overview Logic in Computer Science 68V20, 68V15, 03B35 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. |
| title | Anatomy of a Formal Proof |
| topic | History and Overview Logic in Computer Science 68V20, 68V15, 03B35 |
| url | https://arxiv.org/abs/2411.11885 |