The blueprint standard
What writing a person's reasoning as a tree of checked claims adds to the standard: the statement the person audits, and the claim the person writes. It extends reader-ergonomics: read that one first. Its principles come from the review of autoformalization, and none is measured as a whole loop: they are the conditions under which a topic can be the interface of a person, a model and Lean.
How to use it
- Write each claim to the claim shape, and name it with a
**Shape:**line that links it. - Write to the principles below, and to those of reader-ergonomics and of the topic, which still hold.
- Check: run the standard's checks on the repository.
claim-shapechecks each claim,lean-linkits declaration,comparatorits statement against the challenge file, andtopicthe tree. Lean checks the proofs in CI.
Grades mean what they mean in reader-ergonomics: measured, supported with caveat, convention, not supported. Each principle states its grade and never claims more.
Principles
Statement: what the person audits
| Principle | Claim | Grade |
|---|---|---|
| One claim, one declaration | a claim names exactly one Lean declaration, that declaration exists, and no declaration serves two claims. | convention, adopted: leanblueprint's checkdecls and the projects built on it do the same; no study measured an effect |
| A short statement, apart from its proof | the Lean statement a person audits sits in a short file of its own, apart from every proof, and each proof is held to it. | supported with caveat for people repairing the statement they read and for a precise match to a vetted reference; convention, untested for the loop as a whole |
| The model decides nothing | the person audits the statement that was checked, never a repaired one, and a model's reading of a statement is labelled as a model's, apart from the person's audit. | supported with caveat: model judges overrate translations, and students missed unfaithful steps shown as verified; the two audit columns are a convention, untested |
Claim: what the person writes
| Principle | Claim | Grade |
|---|---|---|
| Guidance at the claim's grain | a verdict, an error or a hint names the person's claim, not the checker's internal step. | supported with caveat: messages at the checker's grain stopped students; convention, untested for the grain itself |
| The person splits the reasoning | each claim is one topic the person wrote, with one sentence, a statement and a proof; the splitting into claims is not left to a model. | convention, untested for the loop; supported with caveat for checking, which small claims help every time practice reports, while help for thinking is reported only where the person did the splitting |
Where the evidence is
Every principle links its review in evidence/, and every work cited is listed once in the bibliography.