From: Viktor Kunčak <firstname.lastname@example.org>
Maybe this is a good point in discussion for me to ask: has anyone looked
whether results such as the PCP theorem can be used to enable large proofs
to be checked at super-linear speed?
The question is not Isabelle specific, but I have not seen it in any
context, from SAT to proof assistants.
Last updated: Dec 08 2021 at 08:24 UTC