Anatomy of a Formal Proof
| Autor: | Avigad, Jeremy, Commelin, Johan, Macbeth, Heather, Topaz, Adam |
|---|---|
| Rok vydání: | 2024 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: 12 pages |
| Databáze: | arXiv |
| Externí odkaz: |
|