What a machine-checked proof means

Before a proof is checked, someone chooses a formal statement. Definitions decide what counts as a number, a set, a solution or a derivative. An omitted hypothesis or a changed quantifier can produce a different theorem that is perfectly provable.

The correspondence between that statement and the intended mathematics is an interpretive obligation. It remains visible in the definitions and interfaces the project chooses.

A tactic can search, simplify or construct a proof. A person can supply the steps; an automated system can supply them too. In a kernel-based assistant, this work produces evidence that the checker must accept.

Proof search can be complicated and unreliable without making every search procedure part of the logical foundation. A failed search usually says that this attempt failed, rather than that the mathematical claim is false.

A kernel checks that the proof follows the rules of its formal system under its declared dependencies. The result concerns the encoded theorem. It does not independently establish that the theorem captures an English manuscript.

The architecture differs across assistants: Lean and Rocq check proof terms; Isabelle's LCF tradition protects the construction of theorem values; Mizar has a different checker structure. How the mechanisms differ explains the trust boundary in detail.

A small result from Whitehead and Russell's Principia Mathematica lets us inspect the correspondence directly. Theorem *54.43 says that two singleton sets are disjoint exactly when their union has two elements. It is the precursor to the famous arithmetic identity; the displayed proposition itself uses set union, not addition.

Write the singletons as S = {a} and T = {b}. Each set contains its displayed point and nothing else. The proof asks how the relationship between a and b controls their intersection and union.

If a differs from b, the singletons share no member. Their ordinary union has exactly the two distinct points a and b. Distinctness therefore connects both sides of the biconditional.

No algorithm for deciding equality on the entire carrier is needed. The proof uses the distinctness evidence supplied in this case.

If a equals b, the two singletons overlap completely. Their ordinary union still contains one point. Any alleged pair of distinct members would both equal that point, giving a contradiction.

There can be two ways to prove membership in that union, one from each input set. Those two receipts of membership refer to the same point; they do not make two set elements.

Our Agda and Arend presentations can retain those witnesses explicitly. The mathematical predicate still counts distinct carrier points. A tagged disjoint sum would create a different carrier, with a left point and a right point even when a equals b.

After choosing representatives of the two singletons, both conditions are equivalent to a differing from b. The final proof joins those two equivalences and eliminates the representatives from its conclusion.

All six new implementations preserve these local landmarks and pass their native checks. The existing Metamath proof also checks, through a different library route. The complete Principia comparison exposes the code, exact versions and historical dependencies.