3 ms·

> 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 ma

by 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.

by CHY872 12y ago

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.