4 ms·
That sounds like the current proof is too brute-force—too badly understood by humans—for humans to be able to explain it to Lean?
by mananaysiempre 1y ago
That sounds like the current proof is too brute-force—too badly understood by humans—for humans to be able to explain it to Lean?