Someone tells you that 8,051 has two factors: 83 and 97. You can inspect the claim with a multiplication. Eighty-three times one hundred is 8,300; subtract three lots of 83, or 249, and the result is 8,051. Both factors are larger than one and smaller than the original number. The claim that the number is composite has a compact witness.
You did not have to discover the factors. The person who supplied them gave you something that makes their particular answer checkable. This small example captures a powerful engineering idea: allow a complicated process to propose an answer, then require evidence that a simpler process can inspect.
A certificate is that inspectable evidence. Its usefulness depends on the exact claim and the checker’s rules. The word does not confer trust on its own.
What the multiplication certifies
For this example, the claim is narrow: the integer 8,051 is composite. A valid certificate gives integers a and b such that 1 < a < 8,051, 1 < b < 8,051, and a × b = 8,051. The pair 83, 97 meets those conditions.
Why include the inequalities? Because the pair 1, 8,051 also passes the multiplication. It proves nothing about compositeness. A checker that inspects only the product has checked a weaker statement than the one the reader cares about.
This is the first trust boundary. Before you discuss how reliable a checker is, decide whether its specification expresses the intended claim. A perfectly implemented check for the wrong property can be perfectly unhelpful.
The arithmetic here is an original teaching example, independently recalculated for this series. It does not establish that finding every certificate is easy, or that every kind of mathematical question has a short certificate. It illustrates a separation of jobs for one claim.
A formal proof as inspectable evidence
A theorem prover extends this idea from a pair of factors to an explicit representation of a proof. Lean, for example, uses a core type theory in which a proof term can be checked against the proposition it is meant to prove. User-facing notation and tactics help produce that term; the trusted kernel checks it.
That architecture is significant because the machinery that proposes a proof can be elaborate. A tactic may search, rewrite expressions or use other procedures. Its success is supposed to leave a term that meets the kernel’s rules. The official Lean description of elaboration and kernel checking explains the separation. This article describes the architecture; it does not claim to have run a Lean proof.
For a proof generated with AI assistance, the same distinction remains useful. A model’s confidence or eloquence is not the certificate. A term accepted by the checker supplies a different kind of evidence. Even then, someone must examine the formal proposition and its assumptions to know whether it answers the original question.
Suppose a requested claim is “every submitted order is charged exactly once.” A proof about a function that maps an already deduplicated list into charges may be valid. It does not establish that the actual input list is deduplicated, or that a retry cannot send a second payment request. The gap lies between the modeled statement and the operating system. This is a hypothetical illustration, not an audit of a payment service.
Assumptions travel with the proof
A proof derives its conclusion from rules, definitions, earlier results and possibly axioms. An axiom is an assumption admitted without proof in that system. The evidence remains conditional on those foundations.
Lean provides an axiom-dependency inspection command, #print axioms, that makes such dependencies visible. Its documentation also describes sorry, a placeholder that can permit an unfinished proof, and native-evaluation methods that enlarge the trusted basis to include compiled computations. Those details are why “the file finished without an error” needs a more careful interpretation than “the desired theorem is established with no extra assumptions.” Lean’s axiom reference gives the examples and dependency rules.
An assumption is not automatically a flaw. Mathematical work legitimately chooses foundations. What matters is whether the assumptions are appropriate, visible and compatible with the conclusion being advertised. A placeholder treated as a finished proof changes the evidential status entirely.
The hardware and checker implementation also matter. A trusted kernel is a component on which the checking result depends; “trusted” names its role, rather than guaranteeing that its implementation has no defects. A small checking basis can make review and independent implementations more feasible. Confidence comes from a chain whose links can be examined.
The checker must keep its own limits
It is tempting to take this architecture a step further. If one checker validates another, and that checker validates another, can the chain eventually certify itself completely?
The proof-limit article explains why sufficiently strong effective consistent formal systems have limits on establishing their own consistency under the usual conditions. That result does not forbid checking a particular execution or proving a specific property of a program in an appropriate formal setting. It does rule out casually treating a tower of checking as an assumption-free final guarantee.
In practice, the builder asks a more bounded question. Which component has authority to accept an output? What assumptions enter its decision? Can it fail safely if evidence is missing or malformed? Is the proposer able to change the rules that judge its own answer?
Keeping proposal and acceptance separate can protect a useful contract. An optimizer may search thousands of schedules; a checker verifies that the submitted one assigns every required job once and respects declared constraints. If the checker accepts only the constraints it actually inspects, it can remain valuable even when the searcher is unpredictable.
However, a feasible schedule is not necessarily the best schedule. If optimality matters, it needs its own evidence. Likewise, a calculation can be internally consistent and still use an obsolete price, a mislabeled unit or a sensor reading from the wrong machine. A mathematical certificate does not discover the provenance of an input unless that is part of the specified claim and evidence.
Why this helps an AI workflow
Language models often provide an explanation after an answer. Some explanations help a person understand; others repeat the answer in a more convincing tone. Asking for an inspectable artifact changes the workflow when the task permits one.
For a factual summary, that artifact might include specific passages and identifiers a reviewer can open. Such citations are evidence pointers, not a formal proof, and must actually support the text. For a numerical answer, the artifact might include inputs, units and a reproducible calculation. For a constrained plan, it might be the plan in a structured form a separate checker can inspect. Each case has a different acceptance standard.
This is where “self-checking” earns a modest, useful meaning. The system carries out checking as part of its operation, while the scope and authority of the check remain explicit. It need not claim universal truth, awareness or freedom from every failure.
The two factors are still the simplest illustration. The answer becomes easier to assess because it brings you the multiplication you need—and because you know why multiplying by one would not satisfy the claim.
Loading comments…