6 ms·
The validity of a mathematical proof depends on a few very precise rules that can be checked by a computer, so I think it's interesting that we still rely so mu
by tprice7 14y ago
The validity of a mathematical proof depends on a few very precise rules that can be checked by a computer, so I think it's interesting that we still rely so much on humans for the verification of mathematical proofs. As the article points out it's clearly problematic.
- sillysaurus 14y agoSure, but then you quickly run into the issue of, "That depends what you mean by 'rule'."
- tprice7 14y agoPlease elaborate. I find it difficult to believe that the problem you are hinting at would be a showstopper because there already exist computer systems for verifying mathematical proofs to standards of rigor acceptable by mainstream mathematicians.
- taligent 14y agoComputers aren't some magical machines that instantly understand what we mean. At some point somebody has to write the code to implement those 'rules'. Which then opens up exactly the same problems (if not more) than if you just verified by hand.
- tprice7 14y agoWell, yes, we would have to convince ourselves of the validity of the code that checks the proofs. But the thing is once we made one proof checker whose code we were really confident about, the checking would be over because we could use it for any proof. Whereas with human verification of proofs each new proof is a new checking job.
- Q6T46nT668w6i3m 14y agoMath is a humanity. Theorems _are_ computationally proven. However, they might not be adopted for humanistic reasons. For example: http://en.wikipedia.org/wiki/Four_color_theorem http://en.wikipedia.org/wiki/Four_color_theorem.
- shadowfox 14y agoI don't know if you have tried to encode a reasonable sized theorem/proof in Coq or Agda. It is worth giving it a shot if you haven't. It is kind of eye opening (and both these systems are significantly different from each other). The real problems I have had with that so far has been a) the extreme precision required in encoding the problem. This exceeds what you normally require in a paper proof b) ensuring that the prover "understands" the necessary background math that you are basing the proof on. i.e. Libraries of math. This situation is improving with time c) The search strategies that the prover is using to verify steps is sub-optimal/does not work for your case. When a human reads/writes/verifies a proof there is a lot of cognitive shortcuts and background information coming in to play. But for a prover this has to be spelled out precisely. Provers tend to come with a set of built-in "tactics" to do this and (often) allow new tactics to be written out. (Coq, for example, allows you to write your own tactics for example. But it is not exactly fun). Again this is slowly improving. For most mathematicians this process is a high overhead one (as yet).
- foobarqux 14y agoMachine checked proofs are intractably long and are not fully automatic except for very simple problems.
- tprice7 14y agoWhat do you mean by not fully automatic? What is the manual part? I think right now the job of describing a (sophisticated) proof to a computer is analogous to the job of writing a sophisticated computer program like a game or Facebook in assembly code. What mathematics needs is a concise language that can easily be understood by people and computers alike, like Python.
- foobarqux 14y agoThe manual part is writing out steps of the proof. Some times these steps can be automated. Usually they are guided by a user. They are typically not written out step by step by hand because it is very tedious. I doubt complicated ideas expressed in advanced mathematical papers can be easily or succinctly expressed formally. http://en.wikipedia.org/wiki/Theorem_prover http://en.wikipedia.org/wiki/Theorem_prover http://www.cs.ru.nl/~freek/100/ http://www.cs.ru.nl/~freek/100/ But more importantly, the objective of a mathematical paper is to get readers to understand the proof, a goal which is poorly achieved with formal verification.
- Evbn 14y agoHave you ever used one of these systems that you claim exists? Math is not mechanically formalized beyond a tiny bit of foundational set theory. Most of modern math is hand waving by brilliant people who trust each others hands, and Doron Zeilberger calling their bullshit and begging them to start being more careful.
- revelation 14y agoSee http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorem http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_t...
- tprice7 14y agoOk, what about it?
- pixl97 14y agoI'm sorry, did you not happen to read that page?
- explicate 14y agoIf my understanding is correct I think he was referring to the fact that even if you have the axioms and an algorithm to figure out all the theorems, you can't prove all the truths. There will be blind spots.
- tprice7 14y agoThank you for the explanation. For a given set of axioms you have the same "blind spots" whether you are verifying proofs manually or with computer assistance.
- fatbird 14y agoThe basic problem with your idea is that significant new proofs usually involve the invention of new branches of mathematics. It's not simply the derivation of new axioms from existing foundations (which fails for reasons outlined below because of Godel's Incompleteness Theorem), it's the laying of new foundations. For a proof checker to check it, it would need to encode those foundations, which is equivalent to discovering the proof itself. Otherwise, given what you say, we could just let proof checkers run on clusters and stop by on Mondays to see what new discoveries have been made :)
- cynicalkane 14y agoI have to say something here, because this is complete nonsense. Nothing in Godel's incompleteness theorems says that new theorems can't be found. It says theorems can't be enumerated, which actually means the opposite--there's always something new to find in a sufficiently strong system of mathematics. Not that there are theorem-enumerators of significant power in the first place. Furthermore, proofs generally do not introduce new axioms and a proof that does, that isn't intended to be foundational, would be considered unsound.
- fatbird 14y agoAgree with everything you say about Godel. I'm not sure what your last line means, though. Speaking strictly in terms of axioms and derived theorems, that seems fine, but in thinking of, say, Wiles' proof of Fermat's Last Theorem, which wended broadly through various branches of math, extending them or perhaps inventing them as needed, it seems incorrect to say this. I'm not sure whether you want to characterize Wiles as introducing new axioms, but he certainly wasn't simply deriving new theorems that could have been computationally enumerated. Perhaps I'm wrong; I'm not a mathematician. But my understanding of Godel, axiomatic systems, and proof engines is that what they do simply isn't comparable to, say, what Mochizuki did with the ABC Conjecture.
- xamuel 14y agoMinor nitpick: Godel does not say theorems can't be enumerated, obviously they can be, just use brute force. Rather it says theorems provable from sufficiently strong axioms can't be decided. So if you want to know whether your axioms prove 1=0, you can start enumerating all the theorems they prove, and if they do prove 1=0, eventually you'll see it, but if not, there's no way to "go far enough" to rule out the possibility that 1=0 will appear later on in the enumeration.