Loading...
Please wait, while we are loading the content...
Similar Documents
What is a proof? What should it be?
| Content Provider | Semantic Scholar |
|---|---|
| Author | Benzmuller, Christoph |
| Copyright Year | 2019 |
| Abstract | Mathematical proofs should be paired with formal proofs, whenever feasible. What is a proof? Is it the rigorous but typically rather unintuitive formal derivation of a new “truth” from its premises using accurately defined rules of inference? Or is it an artful communication act in which the beautiful structures underlying a new mathematical insight are revealed to peer experts in such a way that they can easily see and accept it, and even gain further inspiration? The former notion, referred to as formal proof, is primarily concerned with logical rigor and soundness. Intuition and beauty is still a secondary concern, if at all. Formal proofs have recently attained increased, albeit quite controversial, attention in mathematics. This interest has been triggered by successful applications of modern theorem proving technology to challenging mathematical verification and reasoning tasks. Some of the settled problems are of such a kind, that human cognition alone has apparently reached its limits for attacking them. Respective examples include: 1. Hales’ [13] verification of his proof of the Kepler conjecture within the proof assistant HOL Light: A board of expert reviewers of the Annals of Mathematics had previously surrendered this complex task, but Hales and his team mastered it in interaction with a proof assistant system. As the main result, the computer system produced a formal proof that is now independently verifiable — by humans and/or (other) computer programs. 2. Heule & Kullmann’s [15] automated solution of the Pythagorean Triples Problem: In this work an open mathematical problem was solved with fully automated SAT solving technology. The formal proof that was generated by the computer program is of enormous size (about 200TB). Nevertheless, it is still independently verifiable (at least by machines). This line of research has recently been continued by an automatic solution for Schur Number Five [14]. While some mathematicians embrace this new, computer-supported alternative mathematics, many others still strongly reject it and ask: “Is this still maths?”. Those latter, disapproving mathematicians typically point to the virtues of traditional mathematical proofs, which, in contrast to formal proofs, focus on intuition, beauty and explanatory power. However, such proofs often lack logical rigor, and the exact dependencies and the precisely required inference principles may remain vague — but these weaknesses are considered subordinate to human intuition and abstractlevel understanding. Moreover, the assessment of mathematical proofs is traditionally also handled quite differently from those of formal proofs: it is organized as a kind of social/voting process in which a sufficient number of peers has to be convinced of the new result for it to be generally established. It is thus of little surprise that many mathematical proofs do in fact suffer from mostly minor, but occasionally also major, technical flaws that have escaped the human eye. Most of these errors, I claim, would have been revealed in a formal proof verification process. Both notions of proof thus constitute strong antipodes, with orthogonal pros and cons, and with opposing goals. Traditional mathematical proofs are made for, and consumed by, humans, while formal proofs are predominantly generated with, and consumed by, machines. |
| File Format | PDF HTM / HTML |
| DOI | 10.13140/RG.2.2.13405.87521/1 |
| Alternate Webpage(s) | https://arxiv.org/pdf/1904.06332v1.pdf |
| Alternate Webpage(s) | https://doi.org/10.13140/RG.2.2.13405.87521%2F1 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
