Add autoform skeleton: the trusted surface of a formalized statement

[ArmelRandy]

Summary

This adds the "skeleton" the Atlas release described but did not ship: for each formalized statement, the few lines a person has to read to agree that the Lean says what the book says. It is one new command, autoform skeleton, with its documentation and tests, and it keeps main's contract: Markdown remains the only authority, the output is deterministic and path-free, nothing is written into the vault, and check, audit, and render still never run Lean.

Three follow-ups build on it and are held back so each can be reviewed on its own: read-backs and approvals, kernel-checked probes, and a calibration set with a blind rubric for faithfulness judges.

What it does

For every lean: declaration a blueprint names, a small Lean probe run with lake env lean against the built project computes the closure of the statement: the elaborated signature, the statement as written, and every project definition it rests on, quoted in dependency order, plus the library notions it assumes and the axioms it finally uses. Proofs are never entered. A definition contributes its body as well as its type, since the body is its meaning; a theorem met along the way contributes only its type; constructors, projections, recursors, and matchers fold onto the declaration a reader sees. The closure is computed from elaborated terms rather than source text, because a lexical pass cannot see through open, notation, implicit instances, or variable binders, and every miss silently shrinks the surface a reader is told to trust.

The written statement is cut at the value's byte position with the file's opened namespaces in scope, so scoped notation such as #s or n ! parses and no proof text leaks into the cut; casts are printed with the type they land in, since 1 / ↑n means something else in ℕ than in ℚ.

Each skeleton carries a sixteen-hex hash of its meaning that ignores comments and docstrings, so packets and reports can be compared across builds: two reports differ on it exactly where a statement changed meaning.

Flags, all documented in the CLI reference:

• --output records an autoform-skeleton/v1 report; the text form prints what a reviewer reads.
• --packets writes comment-stripped packets, per declaration and per article, for blind auditors, with a manifest mapping packets to articles and hashes; --passages adds the source passage an article cites through a #L<start>-L<end> locator on a vendored source file, counted as sed counts lines.

Evidence

Exercised on three consumer projects: chapter 1 of Lebl's Basic Analysis I (40 declarations), lectures 1–2 of Etingof's Representations of Lie Groups (9), and chapters 1–2 of Zhao's Probabilistic Methods in Combinatorics (33). Blind auditors working from the packets caught defects in the packet format before reviewing any statement, and a blind judge working from packet and passage found genuine omissions in statements written with care, including a proposition in the notes that is false as stated.

Verification

make lint, make test, and make check-example pass. Two tests build a Mathlib-free fixture project in a temporary directory and run the real probe; they skip when lake or the pinned toolchain is absent, as in this repository's CI, and pass locally with a toolchain.

Notes for review

• The probe program ships as package data under autoform_cli/probes/, deliberately outside templates/, which autoform init scaffolds into consumer projects.
• skeleton is the one command that runs Lean. It needs a built project, exactly as the generated verify workflow does.

🤖 Generated with Claude Code

[meta-cla]

Hi @ArmelRandy!

Thank you for your pull request and welcome to our community.

Action Required

In order to merge any pull request (code, docs, etc.), we require contributors to sign our Contributor License Agreement, and we don't seem to have one on file for you.

Process

In order for us to review and merge your suggested changes, please sign at https://code.facebook.com/cla. If you are contributing on behalf of someone else (eg your employer), the individual CLA may not be sufficient and your employer may need to sign the corporate CLA.

Once the CLA is signed, our tooling will perform checks and validations. Afterwards, the pull request will be tagged with CLA signed. The tagging process may take up to 1 hour after signing. Please give it that time before contacting us about it.

If you have received this in error or have any questions, please contact us at cla@meta.com. Thanks!

[meta-cla]

Thank you for signing our Contributor License Agreement. We can now accept your code for this (and any) Meta Open Source project. Thanks!

[Deicyde]

Review result: changes needed. The current skeleton is not yet a safe approval boundary.

• Source and artifacts are not freshness-bound. After changing a theorem to : True without rebuilding, extraction returned the old elaborated signature, new source text, and the old hash.
• Meaning hashes collide across real semantic changes: macro expansion 1 -> 2, an implicit instance changing a proposition True -> False, "a--b" -> "a--c", and whitespace changes inside string literals.
• The trust closure is incomplete: opaque bodies omit dependencies, dotted Lake roots can classify local declarations as external, and theorem dependencies leak full proof bodies into “proof-free” packets.
• Probe records are weakly schema-checked, and scoped notation state leaks between roots, making output depend on batch membership/order.
• Packet output is written in place, follows existing symlinks, and leaves removed packets behind. --json --packets also writes non-JSON status text to stdout.

These were reproduced against built fixtures. The hash should be based on canonical elaborated expressions and complete trust-boundary identities; extraction must verify source/artifact freshness before emitting an approvable report.

[Deicyde]

I implemented the review fixes in ArmelRandy#1. It is a single commit on top of this PR head, so it can be merged directly into skeleton.

The patch adds freshness checks, canonical elaborated semantic hashes, complete local/external/axiom trust binding, proof-free packet enforcement, strict report validation, safe managed-output replacement, and shared probe caching. Verification: make lint, make test (583 passed, 1 skipped), and make check-example all pass.

[ArmelRandy]

Thank you for reviewing the PR and implementing the fixes. I've merged it into my fork. This skeleton is the first building block in a series of contributions I have in mind. The next one will be a read-back mechanism from Lean to LaTeX, in the spirit of prove2me. It is a way to ease human review by allowing reviewers to quickly compare the "LaTeX rendering" of Lean code against the original source statement.

[Deicyde]

Second pass at 1f0a4e3: the prior review findings are addressed. This tree exactly matches the independently audited helper tree; local verification passed make lint, make test (583 passed, 1 skipped), and make check-example. Upstream Actions still requires maintainer approval before its jobs can run.