3 ms·

Well, the author's point is probably still generally correct - in almost all fields proofs are not presented from axioms, and you could easily go your whole lif

• madez 12y ago
  > I'm sure you can do more interesting things with metamath, but I feel confident in saying that if you're a research mathematician, you'll lose a lot of time learning it and using it. And then save time because you can be sure that the proofs you write are correct. > I'm currently writing my undergraduate project in a proof assistant, and you end up with tonnes of unreadable garbage like ASM_SIMP_TAC (srw_ss ()) [DETERMINACY_LEMMA, simp_expand_def] THEN1 METIS_TAC [] THEN RW_TAC (srw_ss ()) [ss_ecases] THEN FULL_SIMP_TAC (srw_ss ()) []. > which has no real relation to any normal thought. Proving the determinacy of a relation took a matter of days of careful thinking (as a newbie to the package) - despite being able to prove it in a couple of lines of handwritten prose. Did you try isar? > I also think that his line > (it almost certainly is not, but more pertinent, how could you ever be sure it is?) > is still a good point - you're trusting your correctness to a computer program, and all of the libraries built on top of it. The chances that one of these has a bug in (by this I mean a bug in the rules of inference of the theory) that could lead to the theory outputting garbage is probably quite high. It's not at all a good point. There are theorem provers that rely on the correctness of just a very small kernel. Everything on top (libraries) is then guaranteed to follow the rules imposed by the kernel.
  • CHY872 12y ago
    > And then save time because you can be sure that the proofs you write are correct. For better or worse, we both know that's not required to be a successful mathematician. I remember reading a presentation from a guy advocating mechanised proof who realised that almost every important proof in his field had been later shown to be false. > Did you try isar? I had a go at using Isabelle (in general) and truthfully never really got onto Isar - I discovered that both my supervisors have written large theories in HOL4 (JIT compilers etc), but have no recent experience with Isabelle, so that's what I'm using. I've seen examples of Isar which look nice, but I'm skeptical about its scalability. You make a good point, thouugh. > It's not at all a good point. There are theorem provers that rely on the correctness of just a very small kernel. Everything on top (libraries) is then guaranteed to follow the rules imposed by the kernel. Yes, of course - but the richness of a theorem prover comes from the logics you define on top of it. If the library implementation of a particularly complex structure defined externally to the logic with no easy to coverify definition had a mistake in its definition which is not caught, any entailed inconsistencies are transmitted to the theorems that rely on this data structure. Sure, your theorems are correct in the logic - but they might not be useful. I obviously pick the more engineering based example, but that's merely due to my being ignorant of most pure mathematics - there are probably analogues. This is a growing problem for companies like Intel, who use a software model to test their firmwares before the hardware is available [1] - they want to verify that the operations are identical. [1] - http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/44-Formal-Covalidation-Low-Level-Interfaces.pdf http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/44-...
    • madez 12y ago
      > For better or worse, we both know that's not required to be a successful mathematician. I remember reading a presentation from a guy advocating mechanised proof who realised that almost every important proof in his field had been later shown to be false. Some professors I know told me something along those lines about various topics of mathematics. The more advanced the topic gets the less people cope with the complexity. In the end it gets so specialized that only a few people in the world can and are willing to follow the advance. That situation combined with human notorious fallibility brings mathematic research in a very bad situation. I makes me sad - and angry I have to admit - that the professors I met don't recognize computer-aid as the solution. Besides that I personally had the most pleasure doing mathematics while being guarded by a computer against my stupidity[+]. > Yes, of course - but the richness of a theorem prover comes from the logics you define on top of it. > If the library implementation of a particularly complex structure defined externally to the logic with no easy to coverify definition had a mistake in its definition which is not caught, any entailed inconsistencies are transmitted to the theorems that rely on this data structure. > Sure, your theorems are correct in the logic - but they might not be useful. I obviously pick the more engineering based [+] You raise a good point. The computer can't do all the work. Nevertheless it's a huge advance to only have to verify the definitions and theorem statements instead of all that combined with the proofs. It's like having to remember the summary of a book instead of the whole book. Someday we will hit a wall even when using computers but that shouldn't stop us know. > This is a growing problem for companies like Intel, who use a software model to test their firmwares before the hardware is available [1] - they want to verify that the operations are identical. Thats awesome! Nice problem to work on. Stories like this keep my dream alive that there are interesting workplaces in this world.
• bumbledraven 12y ago
  Well, the author's point is probably still generally correct - in almost all fields proofs are not presented from axioms, and you could easily go your whole life as a mathematician without encountering such a proof, except perhaps by accident. His point was that formal proofs are "hypothetical", not that they are rarely encountered. What part of > The trouble is, no one has ever carried out that filling-in process. It’s purely hypothetical. don't you understand? I'm currently writing my undergraduate project in a proof assistant, and you end up with tonnes of unreadable garbage like ASM_SIMP_TAC (srw_ss ()) [DETERMINACY_LEMMA, simp_expand_def] THEN1 METIS_TAC [] THEN RW_TAC (srw_ss ()) [ss_ecases] THEN FULL_SIMP_TAC (srw_ss ()) []. which has no real relation to any normal thought. The syntax you describe bears very little relation to formal system like Metamath in which proofs are readily checkable by people and machines. I also think that his line (it almost certainly is not, but more pertinent, how could you ever be sure it is?) is still a good point - you're trusting your correctness to a computer program, and all of the libraries built on top of it. No. Metamath proofs can easily be verified by hand.
• AngrySkillzz 12y ago
  Similarly, many programmers go their entire careers without touching assembly language or logic gates, yet we all know that our programs can be (and are) distilled down to this. There are definitely people that worry about this, e.g. compiler writers and mathematical logicians, but to most of us it just isn't that important. In addition, it's an abstraction that leaks fairly infrequently, and so far we haven't observed it in the way you're implying; the most prominent "leaks" of mathematical logic are likely unprovability or having to accept stronger axioms to prove a particular statement (e.g. Choice or maybe Grothendieck-Tarski). Addendum: the above is mostly tangential to the original article. The author is very correct that a modern mathematical proof exists, and is formulated to, show another person with suitable background how to work out the truth of a statement. But don't let this form of proof distract you from the existence of the foundations of rigorous proof in general; just as we don't let Ruby's English-like syntax convince us that we aren't truly executing computation. The foundations of mathematical logic are complex, like the transistors on a microchip, but they do "work," in the strongest epistemological sense of the word.
• baddox 12y ago
  Well, the author's point is probably still generally correct - in almost all fields proofs are not presented from axioms, and you could easily go your whole life as a mathematician without encountering such a proof, except perhaps by accident. I find that difficult to believe. My basic math courses in college taught proofs using axioms, starting with really basic stuff like proving that the product of two even integers is an even integer. I don't see how anyone with a mathematics degree could miss that, or could do much useful work without that.