Lean4 Domain Explanation Language (L4DEL)

lean4-explainer reads Lean4 Domain Explanation Language directives from Lean line comments. An annotation is optional at first. The tool checks every directive it finds, and for each declaration without a valid annotation it prints a template to paste in.

Workflow

1. Run lean4-explainer check --lean-root lean to see errors and warnings.
2. Run lean4-explainer annotate --lean-root lean --file Demo/Basics.lean to print templates.
3. Paste a template directly above its declaration and replace every TODO_ value.
4. Run check again. A TODO_ value left behind is a warning, so the build reports it.

Directives

• title: a short heading. At most one.
• intuition: one plain sentence on why the result holds. At most one.
• step: one proof step, in order. Any number.
• prereq: comma-separated fully qualified names the proof depends on.
• see: comma-separated related declarations.
• term: word = definition. Each word is defined once in the project.
• acronym: SHORT = expansion. The expansion appears in the legend at the top of every affected file page. Acronym-looking source text without a supplied expansion is labeled as unresolved; the renderer never guesses what an upstream author meant.
• source: label = https://URL. Repeat it for independent sources.
• quote: source label = exact excerpt. The label must match a source line; the excerpt is rendered as a linked quotation rather than being passed off as the explainer's prose.

Sources and attribution

Use immutable links where possible: a full-commit repository blob for the exact formal source, a DOI or versioned arXiv record for a paper, or a versioned project blueprint. A citation makes an explanation traceable; it does not by itself certify that the explanation is correct.

Rules

Only line comments carry directives. A directive attaches to the next declaration. Anonymous declarations cannot carry directives. Keys are case-sensitive. The full grammar is in the module docstring of lean4_explainer_l4del/grammar.py.

Same-named declarations

Identical copies of a declaration count as one object, so a plain name refers to it. Declarations that share a name but differ in code are distinct definitions. Refer to one as Name@path, for example Demo.value@Var/B.lean.

Example

/-- Three items in two boxes put two items in one box. -/
-- L4DEL: title: Pigeonhole for three items in two boxes
-- L4DEL: intuition: Three items cannot all sit in different boxes when there are only two boxes.
-- L4DEL: step: Assume no box holds two items.
-- L4DEL: step: Then three items need three different boxes, which do not exist.
-- L4DEL: source: Formal statement = https://example.org/pinned-source#L1
-- L4DEL: quote: Formal statement = Three items in two boxes put two items in one box.
-- L4DEL: acronym: DEL = Domain Explanation Language
-- L4DEL: prereq: Demo.box_count
-- L4DEL: term: box = a container for one item
theorem pigeonhole_three_two : ...