Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Cl-isabelle-users Digest, Vol 182, Issue 4

view this post on Zulip Email Gateway (Aug 05 2020 at 12:44):

From: Viktor Kunčak <>
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