Public verifications of Lean solutions

The house runs a three-kernel judge on a solution: Lean FRO's comparator checks that each theorem has exactly the statement fixed by the challenge and uses only permitted axioms, then the official Lean kernel, nanoda and con-leche (a checker proven not to accept a proof of False) replay it. We record the verdict here, signed. We certify acceptance by the named kernels, not absolute truth, and not that the formal statement captures its author's intent.

Keeping your solution sealed? Do not send it here: prove it locally with the ZK program and post only the receipt as a ZK certificate. The receipt is verified mathematically; your proof never leaves your machine. Certificates

No verifications yet.