4 ms·

Once again, this is a rather perfect example of why there is a great need in Math for a universal formal proof language that can be verified by computers. If t

Once again, this is a rather perfect example of why there is a great need in Math for a universal formal proof language that can be verified by computers. If this existed, the burden of proof would be on Mochizuki to present his proof in a language that can actually be understood by others and by machines.

QuesnayJr 7y ago
The problem is that producing a formal proof that can be verified by a computer is incredibly boring. Since it's incredibly boring, nobody is going to do it. It's not a matter of a universal formal proof language existing (there are lots of frameworks that are powerful enough), it's matter of one being easy enough to use that people will willingly use it.
- ur-whale 7y ago
  > The problem is that producing a formal proof that can be verified by a computer is incredibly boring One can't help but wonder: as boring as reading through inter-universal teichmuller theory?
  - Grue3 7y ago
    Well, suppose you want to prove another result similar to abc conjecture. What would you rather read, a formal proof (basically low-level machine code), or an actual human description of a theory used to produce the result?
- gravypod 7y ago
  What would need to exist to make such a proof specification utility less boring? I know many engineers who never thought they'd use unit tests until I was able to demonstrate immediate workflow benefit that made their job far easier than before. If you have experience in higher math, what would need to exist to make such specification useful?
  - QuesnayJr 7y ago
    The challenge is making a tool that's sufficiently ergonomic. It's the UI problem from hell. The problem is that people are much smarter than computers, so you can just specify the broad strokes and your audience can fill in the details as needed.
  - Jweb_Guru 7y ago
    For starters, it would be nice to be able to make trivial manipulations of algebraic expressions involving real numbers not incredibly tedious. As far as I know no existing proof assistant is up to that challenge. Again, it's not a matter of power--many, many proof assistants can formalize the vast majority of mathematics--it's about UX.
wolfgke 7y ago
For example Alexander Grothendieck did not care much about the formal logical foundation of his work. So, I believe that this would make it highly complicated to even formulate some very new math at the borderlands of our knowledge.
- Koshkin 7y ago
  Well Category Theory is a pretty solid logical foundation...
  - wolfgke 7y ago
    Category theory depends on set theory. Unluckily, formulating a category of all sets/groups/rings/... is not easy because there exists no "set of all sets/groups/rings/...". One way to solve this problem is to replace ZFC by its non-conservative extension Tarski–Grothendieck set theory https://en.wikipedia.org/w/index.php?title=Tarski%E2%80%93Grothendieck_set_theory&oldid=918247704 https://en.wikipedia.org/w/index.php?title=Tarski%E2%80%93Gr... to ensure that a Grothendieck universe https://en.wikipedia.org/w/index.php?title=Grothendieck_universe&oldid=899048612 https://en.wikipedia.org/w/index.php?title=Grothendieck_univ... always exists.
    - QuesnayJr 7y ago
      Most of category theory as used in ordinary mathematics can be formulated in ZFC. The category of all groups, etc. is just a propositional formula. If you prefer to explicitly talk about classes, then you can go with NBG, which is a conservative extension of ZFC. Grothendieck needed an extra axiom because he wanted to consider large Grothendieck topologies. The consensus seems to be that universes are avoidable: https://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof https://mathoverflow.net/questions/35746/inaccessible-cardin...

QuesnayJr 7y ago

The problem is that producing a formal proof that can be verified by a computer is incredibly boring. Since it's incredibly boring, nobody is going to do it. It's not a matter of a universal formal proof language existing (there are lots of frameworks that are powerful enough), it's matter of one being easy enough to use that people will willingly use it.

ur-whale 7y ago
> The problem is that producing a formal proof that can be verified by a computer is incredibly boring One can't help but wonder: as boring as reading through inter-universal teichmuller theory?
- Grue3 7y ago
  Well, suppose you want to prove another result similar to abc conjecture. What would you rather read, a formal proof (basically low-level machine code), or an actual human description of a theory used to produce the result?
gravypod 7y ago
What would need to exist to make such a proof specification utility less boring? I know many engineers who never thought they'd use unit tests until I was able to demonstrate immediate workflow benefit that made their job far easier than before. If you have experience in higher math, what would need to exist to make such specification useful?
- QuesnayJr 7y ago
  The challenge is making a tool that's sufficiently ergonomic. It's the UI problem from hell. The problem is that people are much smarter than computers, so you can just specify the broad strokes and your audience can fill in the details as needed.
- Jweb_Guru 7y ago
  For starters, it would be nice to be able to make trivial manipulations of algebraic expressions involving real numbers not incredibly tedious. As far as I know no existing proof assistant is up to that challenge. Again, it's not a matter of power--many, many proof assistants can formalize the vast majority of mathematics--it's about UX.

wolfgke 7y ago

For example Alexander Grothendieck did not care much about the formal logical foundation of his work. So, I believe that this would make it highly complicated to even formulate some very new math at the borderlands of our knowledge.

Koshkin 7y ago
Well Category Theory is a pretty solid logical foundation...
- wolfgke 7y ago
  Category theory depends on set theory. Unluckily, formulating a category of all sets/groups/rings/... is not easy because there exists no "set of all sets/groups/rings/...". One way to solve this problem is to replace ZFC by its non-conservative extension Tarski–Grothendieck set theory https://en.wikipedia.org/w/index.php?title=Tarski%E2%80%93Grothendieck_set_theory&oldid=918247704 https://en.wikipedia.org/w/index.php?title=Tarski%E2%80%93Gr... to ensure that a Grothendieck universe https://en.wikipedia.org/w/index.php?title=Grothendieck_universe&oldid=899048612 https://en.wikipedia.org/w/index.php?title=Grothendieck_univ... always exists.
  - QuesnayJr 7y ago
    Most of category theory as used in ordinary mathematics can be formulated in ZFC. The category of all groups, etc. is just a propositional formula. If you prefer to explicitly talk about classes, then you can go with NBG, which is a conservative extension of ZFC. Grothendieck needed an extra axiom because he wanted to consider large Grothendieck topologies. The consensus seems to be that universes are avoidable: https://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof https://mathoverflow.net/questions/35746/inaccessible-cardin...