Stream: Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 05 2020 at 12:44):

From: Viktor Kunčak <vkuncak@gmail.com>
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?

https://www.youtube.com/watch?v=1wNIvo7jwzc&list=PLm3J0oaFux3ZYpFLwwrlv_EHH9wtH6pnX&index=96

The question is not Isabelle specific, but I have not seen it in any
context, from SAT to proof assistants.

Thanks,

Viktor

Last updated: Jul 15 2022 at 23:21 UTC