4 ms·

I think it is the future. Writing a mathematical proof is writing a computer program. I think it is common to see lots of lets say hacky, untyped work, like som

by foxes 5y ago

I think it is the future. Writing a mathematical proof is writing a computer program. I think it is common to see lots of lets say hacky, untyped work, like some janky bash script, that takes you on some adventure, that you have to spend extra work exploring. Imagine instead reading some declarative program. Everything formalised, use of higher order functions/constructs when appropriate that encapsulate important generalisable ideas (eg in the programming example using "map" when you want to loop over some list). Hacky stuff is fine for exploration and experimentation. But something for publication should be clear. You could use engineering principles, optimising your proofs for readability and efficiency, version control. Seems like it is the future. Disclaimer I have written many "hacky" proofs.

bmitc 5y ago
I am of the opinion that mathematics is very much a human endeavor. Writing a proof is to convince other mathematicians that it’s true. While formalized mathematics is one such technique, I don’t believe it will replace how mathematics is generally done. Writing a program is something different entirely. One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot.
- 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.
- Ericson2314 5y ago
  I rather read some thing that's formal and readable, than just merely readable. > One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot. ~Goëdel~ Gödel's theorems are not relevant. Consider even if the halting problem had the other answer, it still could be impractical to do the brute force search. Same thing here. And frankly, the formal methods community is sick of people spreading FUD from that stuff. Mixing romantic humanism with technical misunderstandings is no good.
  - hollerith 5y ago
    It is spelled Gödel or (in case you cannot put the 2 dots over the "o") Goedel.
    - Ericson2314 5y ago
      Yes thank you. I guess I mixed up US keyboard vs phone typing rather hilariously.
  - bmitc 5y ago
    I didn’t mention Goedel’s theorems, so I don’t know what they’re relevant or irrelevant to, and I am not spreading anything. Maybe I didn’t make that part clear, but it’s more of a question of mine than a statement. It seems to me there would be problems and limits but I haven’t seen them addressed in a way I understand, so the questions and misunderstandings remain. If you have any references, then by all means share them. > Mixing romantic humanism with technical misunderstandings is no good. I think this miscategorizes what I wrote. One could easily do the same. Mathematics is indeed a human endeavor, as are its goals. If machines are to help, then that’s absolutely great (I’m actually a big fan of computers being used to augment human endeavors), but making grand sweeping claims like I’ve seen in discussion of proof assistants is as romantic as anything.
    - foxes 5y ago
      I think the proof assistants are getting very powerful, eg: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... State of the art research explored with lean. I think a certain level of hand wavy romanticism is fine for a HN comment if it can inspire people to be interested in the field. I also would prefer to be corrected in a reasonable discussion than a silent chilling downvote.
- mbrodersen 5y ago
  I am of the opinion that software development is very much a human endeavour as well ;-)
- mbrodersen 5y ago
  Mathematics is not Computation. Mathematics is about stating definitions and prove theorems about those definitions. A mathematician doesn’t care whether those definitions are computable. Take a look at the leading edge (the mathlib community using the Lean prover). A lot of their definitions are non-computable and it works fine.

by foxes 5y ago

bmitc 5y ago

I am of the opinion that mathematics is very much a human endeavor. Writing a proof is to convince other mathematicians that it’s true. While formalized mathematics is one such technique, I don’t believe it will replace how mathematics is generally done. Writing a program is something different entirely. One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot.

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.
Ericson2314 5y ago
I rather read some thing that's formal and readable, than just merely readable. > One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot. ~Goëdel~ Gödel's theorems are not relevant. Consider even if the halting problem had the other answer, it still could be impractical to do the brute force search. Same thing here. And frankly, the formal methods community is sick of people spreading FUD from that stuff. Mixing romantic humanism with technical misunderstandings is no good.
- hollerith 5y ago
  It is spelled Gödel or (in case you cannot put the 2 dots over the "o") Goedel.
  - Ericson2314 5y ago
    Yes thank you. I guess I mixed up US keyboard vs phone typing rather hilariously.
- bmitc 5y ago
  I didn’t mention Goedel’s theorems, so I don’t know what they’re relevant or irrelevant to, and I am not spreading anything. Maybe I didn’t make that part clear, but it’s more of a question of mine than a statement. It seems to me there would be problems and limits but I haven’t seen them addressed in a way I understand, so the questions and misunderstandings remain. If you have any references, then by all means share them. > Mixing romantic humanism with technical misunderstandings is no good. I think this miscategorizes what I wrote. One could easily do the same. Mathematics is indeed a human endeavor, as are its goals. If machines are to help, then that’s absolutely great (I’m actually a big fan of computers being used to augment human endeavors), but making grand sweeping claims like I’ve seen in discussion of proof assistants is as romantic as anything.
  - foxes 5y ago
    I think the proof assistants are getting very powerful, eg: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... State of the art research explored with lean. I think a certain level of hand wavy romanticism is fine for a HN comment if it can inspire people to be interested in the field. I also would prefer to be corrected in a reasonable discussion than a silent chilling downvote.
mbrodersen 5y ago
I am of the opinion that software development is very much a human endeavour as well ;-)
mbrodersen 5y ago
Mathematics is not Computation. Mathematics is about stating definitions and prove theorems about those definitions. A mathematician doesn’t care whether those definitions are computable. Take a look at the leading edge (the mathlib community using the Lean prover). A lot of their definitions are non-computable and it works fine.