3 ms·
So it's 23 years passed and are there any practical implementations that mathematicians would use? Since this work can be applied only to proofs that were reco
by deepsun 11y ago
So it's 23 years passed and are there any practical implementations that mathematicians would use?
Since this work can be applied only to proofs that were recorded in machine-readable format (like Mizar), I suppose it's much harder _to record_ a proof in machine-readable format, than to really go ahead and check all the pages manually.
- pmiller2 11y agoNot that I know of, for the reasons you suggest. AFAIK nobody is seriously using formats like Mizar when we have actual proof assistants available that can check the proof, which kind of obviates the need to use the PCP theorem at all.
- nickpsecurity 11y agoWould there be any remaining value for such a tool in checking proofs if already using a standard, proof-checker? Sort of a "get's it done faster/easier" argument or perhaps like in software a "catch obvious problems in ill-specified work earlier" sort of thing?