3 ms·
Question: Is the computational cost of verifying the proof significantly less than the computational cost of creating the proof?
by bravura 1y ago
Question: Is the computational cost of verifying the proof significantly less than the computational cost of creating the proof?
- crdrost 1y agoLike I haven't run Coq but I assume that in this particular instance, the answer is a rather trivial "yes"? You'd think about, creating this proof is a gigantic research slog and publishable result; verifying it is just looking at the notes you wrote down about what worked (this turing machine doesn't halt and here's the input and here's the repetitive sequence it generates, that turing machine always halts and here's the way we proved it...). But taken more generally, not for this specific instance, your question is actually a Millenium Prize problem worth a million dollars.
- LegionMammal978 1y agoIn principle, you could reduce the problem into running a few very costly programs, so that the proof is completely verified as soon as someone eats that cost. (Some 6-state machines are already looking like they'll take a galactic cost to prove, and others will take a cost just barely within reason.) But this definitely isn't the case for the BB(5) project.
- LegionMammal978 1y agoThe compiled proof does take a few hours to finish verifying on a typical laptop. But obviously the many experiments and enumerations along the way took much more total processing power.
- tsterin 1y ago45 minutes on 13 cores on a standard laptop :)
- Kranar 1y agoThis is true in general for every mathematical proof in ZFC (and even in more powerful theories). The decision problem "Given a formula F and an integer n, is there a ZFC proof of F of length <= n?" is NP complete, meaning that verifying the proof can be done in polynomial time while deriving the proof can require an exponential amount of time.