Blueprint

A person's reasoning written as a tree of topics, each part with a checker, Lean for logic first. A language model interprets the verdicts and guides, so the person does not get lost and the reasoning can be communicated. Formal mathematics calls such a graph of checked claims a blueprint.

This page in French: README.fr.md.

Audit (2026-11-03): the three claims' prose was verified against Euclid IX.20 (Joyce 1996) and its factorial variant (Wikipedia 2026 Euclid) by a model on the maintainer's order, not by a person; the Lean statements wait for a reader of Lean.

Status (2026-11-03), release 0.1.0: the review of autoformalization is done, grey and formal, 273 sources, and names its baseline, B1. B1 is built in miniature, except the audit: Euclid's theorem as a theorem topic and three claim topics, each naming one Lean declaration (design), with a challenge file that holds the four statements apart from the proofs (0006). Five checks run in CI: the topic check, a claim check, a link check, a comparator, and Lean. The card holds five principles and one shape, the claim. The maintainer has not yet compared the statements with their source. The model is not in the loop yet. The work began in reader-ergonomics-topic and moved here with its history (0001).

How it is made: with Claude, an AI assistant by Anthropic, under the maintainer's direction, the way reader-ergonomics was made. Corrections are welcome as issues.

Take it

The blueprint is meant to be copied and kept as your own. Copy it from a tagged release (tags), so a later change here never changes your copy.

Copy shapes/claim.md, the shape, and the checks in checks/local/: claim_shape.py, lean_link.py, comparator.py and topic.py, into the same paths of your repository.
Write each step of your reasoning as a claim topic, and name one Lean declaration on its Lean: line. Keep the statements to audit in a challenge file, apart from the proofs, as Blueprint/Challenge.lean does.
Add checks/config.toml with extends = "reader-ergonomics" and the tables of this repository's own for [topic], [claim_shape], [lean_link] and [comparator]; set their paths to yours.

Pin the standard by commit and run the checks, one command:

git clone https://github.com/Tewf/reader-ergonomics ../reader-ergonomics
git -C ../reader-ergonomics checkout 2e5b6f0c3e67d2dc8195a63cf882d46170e79a5a   # v1.21.0
python3 ../reader-ergonomics/checks/run.py .

Lean is built apart, in CI, with lake build; the checks read the declarations' names and never run Lean.

A disagreement has three places to go:

your reader style, as an override with its reason, when it is about your reader;
an extension, when it is about a genre;
an issue on this repository, when its evidence or its shape is wrong.

The standard's section, Take your own version, gives the rest.

Where it sits

It builds on the topic (reader-ergonomics-topic v0.6.0): every node of a blueprint is a topic, with its title, its summary, its parts as contents and what it uses as links.
It obeys reader-ergonomics (v1.21.0) and runs its checks in CI.
It links down only. Both are pinned by commit; neither links up to this repository.

The loop

The person writes topics; checks in CI return findings to the model; the model translates a formal topic into Lean, which returns errors and goals left open; the model returns guidance to the person: what to split, what is unclear, what the proof assistant rejected, and why.

Graphviz source

// The loop of the AI-augmented topic: the figure of ai-augmented/README.md.
// Colours: one per kind of part, the same in every figure of this extension; each kind is also named in its box.
// person orange, program blue, model green, proof assistant blue (a program); a back edge returns to its sender.
digraph loop {
  graph [rankdir=TB, nodesep=0.5, ranksep=0.55, bgcolor="white", pad=0.2, fontname="Inter"];
  node  [shape=box, style="rounded,filled", fontname="Inter", fontsize=13, margin="0.2,0.1", penwidth=1.5, fontcolor="#1F2328"];
  edge  [fontname="Inter", fontsize=11, color="#3D434B", fontcolor="#55575F", penwidth=1.3, arrowsize=0.8];
  P [label=<<b>person</b><br/><font point-size="11" color="#55575F">writes the idea as topics: one claim</font><br/><font point-size="11" color="#55575F">each, its summary, its parts</font>>, fillcolor="#FBEDE4", color="#B4541A", penwidth=2.6];
  C [label=<<b>checks, in CI</b><br/><font point-size="11" color="#55575F">the form: title, summary, one claim</font><br/><font point-size="11" color="#55575F">per topic, every part listed</font>>, fillcolor="#E8EEF8", color="#2F5DA8"];
  M [label=<<b>model</b><br/><font point-size="11" color="#55575F">explains findings, proposes clearer</font><br/><font point-size="11" color="#55575F">wording; translates a formal topic</font><br/><font point-size="11" color="#55575F">into Lean</font>>, fillcolor="#E6F2EA", color="#2E7D4F"];
  L [label=<<b>proof assistant</b><br/><font point-size="11" color="#55575F">Lean checks the reasoning</font>>, fillcolor="#E8EEF8", color="#2F5DA8"];
  P -> C [label=" topics"];
  C -> M [label=" findings"];
  M -> L [label=" Lean"];
  L -> M [label=" errors, goals\l left open\l"];
  M -> P [label=" guidance: what to split, what is\l unclear, what the proof assistant\l rejected, and why\l"];
}

The figure reads from the person downward; what comes back, errors and goals to the model and guidance to the person, runs upward. Each part has one role:

Part	Role	Decides
person	owns the reasoning; writes each step as a topic	what is claimed
checks	programs: the topic check and the reader-ergonomics checks	whether the form is clear
model	a language model: explains, proposes, translates	nothing: its output is always checked
proof assistant	Lean, for what is formalized	whether the reasoning is valid

Scope

	What	Why
in	any reasoning or creation, written as a tree or graph of topics	a topic can hold any information
in	the topic's properties on every node: title and summary, parts as contents, uses as links, no cycle, three levels in view	the person does not get lost, and the reasoning can be communicated
in	a checker for each part	each claim is checked where it stands, not the whole at the end
in	Lean as the oracle for logic and proofs, the first and for now only checker of meaning	its verdict is exact
in	the model as interpreter of the verdicts and as guide; it decides nothing and never splits for the person	conditions 2 and 4 of the review's position
later	other checkers (sources, tests, specifications), after a review of assurance cases	a claim split into sub-claims each backed by evidence is what systems engineering calls an assurance case
out	building a prover or training a model	others do it; this uses them
out	the topic template itself	reader-ergonomics-topic holds it; this repository pins a release

What the review found

The review reads 80 grey and 182 formal sources, with 11 linked from sibling reviews.

No program decides whether a formal statement means what its source means; research measures it against people or a vetted reference.
Model judges overrate translations: one translator scored 97.5% by its judge and 62.7% by people. Benchmarks' own human-written statements are wrong in 16.4% and 38.5% of two benchmarks.
For a model, the checker's error message is what makes repair work; for people, no study of a proof assistant's messages was found.
Splitting reasoning into small claims helps checking every time, and thinking only where the person did the splitting; no randomised trial was found.

The baseline

B1, the audited blueprint (baseline):

a blueprint of small lemmas, each statement copied from its source;
a model may write proofs, and decides nothing;
Lean checks every submission in CI, and comparator checks that each proof proves the stated claim;
a person audits each statement against its source.

The audit of B1: the maintainer compares each of the four statements in the challenge file with its source and writes the date on the topic's Audited: line. The comparator and the challenge file are in; the audit is the one part of B1 that is not.
Then the loop: the model's place in it, as interpreter and guide, measured against B1.
Before any checker other than Lean: a review of assurance cases, the field's name for the general case.

Part	Summary
standard	the card: five principles, two of them on the statement a person audits and two on the claim a person writes, each with its grade
principles	one file per principle, with its claim, grade, evidence and check
shapes	the claim: the skeleton of one claim of a proof, with the three claims of Euclid's theorem as its examples
design	the designs proposed before a build: the first build is Euclid's theorem as topics checked by Lean
proofs	Euclid's theorem as a theorem topic and three claim topics, each naming its Lean declaration
evidence	the review behind the repository: autoformalization, grey and formal, and its bibliography
decisions	one record per choice that shapes this repository, each opening with the decision in one sentence

Check it

git clone https://github.com/Tewf/reader-ergonomics
python3 reader-ergonomics/checks/run.py path/to/this/repository

CI runs the same checks on every push, at the commits checks.yml pins.

Licence

Code under the Apache License 2.0; prose under CC BY 4.0. Reuse it as you wish, with credit to this repository; CITATION.cff gives a citation if you need one.