Comment by black_knight
1 day ago
Leans proof checker is not polynomial time, unfortunately. It is super exponential. Basically, because it can verify the result of any function it can prove to be total.
1 day ago
Leans proof checker is not polynomial time, unfortunately. It is super exponential. Basically, because it can verify the result of any function it can prove to be total.
That's fine, we just change the problem from "find a lean proof of length < f(n)" to "find a lean proof that can be validated in time < f(n)".
Oh that’s unfortunate.