3 ms·
When you get to the symbols, all becomes symbol manipulation, so why would computer proof verification systems not be up to the task?
by throwaway_pdp09 6y ago
When you get to the symbols, all becomes symbol manipulation, so why would computer proof verification systems not be up to the task?
- tromoi57 6y agoWell, climbing Mt. Everest is also "just moving your arms and legs". But I'm not up to that task! It's certainly possible in principle, but whether it's possible in practice is part of the challenge. You need enough people that understand the details of the proof, and know how to turn that into a formally verified proof. Such proofs can also become slow, so to keep things practical, you also need to take speed into account.
- Ericson2314 6y ago"Quantity has a quality all its own" Also, and perhaps easier to wrap one's head around, is issues of tooling. Already, there is a very heavy use of "tactics" (metaprograms, and ones with decent computational complexity (think "search" not just "expansion")). Mathematicians write lemmas so we can try to run the tactics on "mini problems" that do not grow even as the total body of work grows, but there's always a risk the that there's some sticking point one cannot break down enough.
- pfortuny 6y agoRemember Pentium’s division bug (on mobile so cannot cooy-paste). We need some king of certificate of proof, not just some black-box which answers “OK”, “NOT-OK”.
- Ericson2314 6y agoThe theorem proves that are discussed here already do that.
- kevinbuzzard 6y agoblah blah blah type checkers blah blah blah can be run on different chipsets / OS's blah blah blah computers are several orders of magnitude more accurate blah blah blah not really the issue.