3 ms·
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.
by 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 agoWell, 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 agoWhat 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 agoThe 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 agoFor 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.