Why a kernel, and not a committee

A conventional proof is checked by people. A referee reads the argument, forms a judgement, and the judgement is trusted because of who made it. That process works, but it cannot be run by an incentive mechanism: it is slow, it is expensive, and two competent referees can disagree.

A Lean proof is checked by a kernel. The kernel does not form a judgement. It checks that a term inhabits a type, and it either does or it does not.

What this buys us

The risk moves. With a referee, the question is whether the argument is right. With a kernel, the argument is either accepted or it is not — and the remaining question is whether the formal statement faithfully captures the original conjecture.

That is a narrower and more honest place to put the risk. A statement such as

$\{(n, k) \mid 0 < k \wedge 2k \le n \wedge \mathrm{minFac}\left(\binom{n}{k}\right) > \max(n/k, k)\}\ \text{is finite}$

can be read, argued about and corrected by anyone. Whether a two hundred line tactic proof is sound cannot.

What it does not buy us

Kernel acceptance is necessary but not sufficient. A proof can be accepted and still not deserve a reward — because it was copied from an unmerged pull request, or because it exploits a weakness in the kernel rather than proving the statement.

That is why every accepted proof is held for review before a bounty is issued, and why the grounds for rejection are published before anyone spends a credit. If a human can overturn the kernel, the reasons had better be written down in advance.