5. Read the checking evidence
Your goal is to explain an accepted result together with its conditions. We will compare a complete proof, a proof that uses a hypothesis, and a declaration with an unfinished proof.
A proof can depend on a local hypothesis
theorem from_hypothesis (P : Prop) (h : P) : P := h
#print axioms from_hypothesis
Here P is a proposition and h is an assumed proof of it. The body returns h. The whole theorem says that, given a proposition and a proof of it, you can supply a proof of that proposition.
This is valid, but it does not give a proof of an arbitrary P without the hypothesis. The parameter h remains part of what the theorem requires.
Lean reports no axiom dependencies for this theorem. Local parameters and hypotheses are accounted for in its type; they are not global axioms to be listed by #print axioms.
Here is a small illustrative evidence record for a reading of the local term h. It is a worksheet, not a captured reader result:
| Item | Recorded information in this example |
|---|---|
| Term | h |
| Inferred type | P |
| Local context | P : Prop, h : P |
| Typing outcome | Accepted |
| Formation of the inferred type | P is established as a proposition. |
| Axiom audit for the typing declaration | No recorded axiom dependencies. |
Exercise 5.1. A reader shows a term supplying a proof of P, with h : P in its context and no recorded axiom dependencies. Can you conclude that it establishes P without assuming h?
Hint
The axiom list and the local context answer different questions.
Worked answer
No. You must retain the local context when explaining the result. An empty axiom list does not remove its hypotheses. Conversely, listing a context entry does not by itself tell you whether a particular term uses that entry; that requires information beyond its availability.
Examine an unfinished proof
Now read this deliberately incomplete example:
theorem claimed : 2 + 2 = 5 := sorry
example : 2 + 2 = 5 := claimed
#print axioms claimed
sorry is a placeholder for a missing proof. Lean accepts this file while warning that the declaration uses sorry. The axiom report for claimed includes sorryAx, the placeholder dependency.
Using the declaration again does not complete its proof. The second line uses the proof term represented by claimed, with that same dependency.
The arithmetic claim is false for natural numbers. The accepted typing result is relative to an environment containing the placeholder dependency; it is not a proof of the arithmetic claim independent of that dependency.
Download Evidence.lean to compare both examples and their axiom reports. The placeholder is intentional in this teaching example. It is not needed by any of the completed proofs in the other downloads.
Read the supply statement with its audit
In the source reader, a proof-supply reading requires both:
- An accepted typing outcome for the term.
- Established proposition formation for its inferred type.
This supports reading the term as supplying a proof in the captured environment and context. The same block lists the full context and, immediately beside the supply statement, the axiom dependencies of the relevant typing declaration. If that audit is unavailable, it gives the reason instead.
Read these together. An empty audit attached to a different formation check cannot stand in for the audit of the typing declaration. Nor does an unavailable audit mean “no dependencies.”
An explicit foundational axiom and an unfinished proof placeholder also have different explanatory roles. Report the actual dependency rather than flattening all cases into either “verified” or “unverified.”
Keep different kinds of evidence distinct
| Information | What it tells you |
|---|---|
| Context | Which declarations and entered binders are available, including local definitions and recorded auxiliary entries. |
| Typing outcome | Whether the particular submitted declaration was accepted, rejected, or left unknown in the captured environment. |
| Formation evidence | Whether an occurrence is established as a proposition, type, or other supported kind of expression. |
| Axiom audit | The recorded global axiom dependencies of the relevant declaration, or why they are unavailable. |
| Diagnostic | A warning or error reported during elaboration, which is distinct from an individual checking outcome. |
The reader reference explains how one check can serve multiple roles and how the reader keeps expressions, relations, and outcomes distinct.
Exercise 5.2. A hypothetical inspection has an accepted typing outcome whose audit lists sorryAx. Another check has an empty audit. A learner writes: “All outcomes were accepted, and the panel contains an empty audit, so the equality is proved without assumptions.” Identify the errors.
Worked answer
The relevant typing declaration still depends on sorryAx. The empty audit belongs to another check and cannot replace it. Acceptance must be read relative to the captured environment, and the local context must also be retained. The summary has combined information from different records and discarded a material dependency.
This is an evidence-reading exercise, not a transcript of a captured session.
Carry the evidence with the reading
A saved record does not establish that its outcomes describe the current buffer or imports. The editor-context reference explains freshness and saved-data limits. These lessons supply source files and explanatory worksheets; the optional editor activities make their own captures.
A checked proof term, an interpretation of its type, and a drawing of that interpretation are different objects. A successful check of one does not automatically certify all the others.
Definograph has formal reconstruction results for named representations, with precise conditions. They support the foundation but do not yet establish the complete guarantee for every valid Lean statement and its actual rendered diagram. See the formal foundations reference for the results and their boundaries.
For a particular reading, follow the chain you now know: expression, context, recorded relation, applicable outcome, and dependency audit. Then assess whether the explanation and drawing preserve that information.
← Laws and owners · Tutorial contents · Next: An unfamiliar structure →