4 ms·

A verified proof is a very convincing argument. I am not against including a human focused discussion of a proof, stepping through it in human terms. A verifie

by foxes 5y ago

A verified proof is a very convincing argument. I am not against including a human focused discussion of a proof, stepping through it in human terms. A verified proof is more like the final step or output. I agree this is not how maths is done, there is a huge exploration stage. People do not just crank out a proof even though sometimes it is written in a way to make you believe that. You can spend days, weeks, months exploring. But at some point you should try to formalise that into something coherent. Amendment: this seems to be a very controversial discussion with wildly swinging upvotes/downvotes. I hope people would elaborate on their viewpoints.

bmitc 5y ago
I think it’s all great. I have been interested in picking up something like Coq before. I only made my comment to reflect my personal tempered expectations. Maybe I am completely wrong, but just don’t see how it could wholly replace how mathematics is done and generated, but I do see how it could helpfully augment. I think the analogy is in the fancy type system programming languages like Haskell and Idris and the like, which are not practically affecting how people generally write programs and build systems. In both mathematics and writing programs, one must come up with something that models the solution needed for a given problem or system even if one can formally verify it afterwards, but that first part is the hard part (especially in programming since the assumptions in mathematics are quite explicit and known). I suppose there could be or are systems that generate techniques and proofs rather than merely verify, but I can only imagine that being an intractable problem and one not likely to be practically solved soon.
- foxes 5y ago
  Yes, the stack of papers at my desk with random scribbles are a far cry from a verified proof written in lean. There is lots behind a proof that you don't necessarily see reflected in a piece of code/proof. So I agree, something formal is like a final step.
throwaway81523 5y ago
Proofs are more about understanding why something is true, than verification per se. See this well known article by the illustrious Bill Thurston (RIP): https://arxiv.org/abs/math/9404236 https://arxiv.org/abs/math/9404236
- zozbot234 5y ago
  The free refactorability of a fully formalized proof can provide a lot of additional understanding, compared to an informal sketch.

by foxes 5y ago

bmitc 5y ago

I think it’s all great. I have been interested in picking up something like Coq before. I only made my comment to reflect my personal tempered expectations. Maybe I am completely wrong, but just don’t see how it could wholly replace how mathematics is done and generated, but I do see how it could helpfully augment. I think the analogy is in the fancy type system programming languages like Haskell and Idris and the like, which are not practically affecting how people generally write programs and build systems. In both mathematics and writing programs, one must come up with something that models the solution needed for a given problem or system even if one can formally verify it afterwards, but that first part is the hard part (especially in programming since the assumptions in mathematics are quite explicit and known). I suppose there could be or are systems that generate techniques and proofs rather than merely verify, but I can only imagine that being an intractable problem and one not likely to be practically solved soon.

foxes 5y ago
Yes, the stack of papers at my desk with random scribbles are a far cry from a verified proof written in lean. There is lots behind a proof that you don't necessarily see reflected in a piece of code/proof. So I agree, something formal is like a final step.

throwaway81523 5y ago

Proofs are more about understanding why something is true, than verification per se. See this well known article by the illustrious Bill Thurston (RIP): https://arxiv.org/abs/math/9404236 https://arxiv.org/abs/math/9404236

zozbot234 5y ago
The free refactorability of a fully formalized proof can provide a lot of additional understanding, compared to an informal sketch.