Agent-assisted work and human examination [connes-000T]

✍️sourceAGENTDRAFTED

This draft expands the examination method summarized in § [connes-000Z].

An agent-authored formalization is easier to examine when the code comes with a route back to the literature, an executable verification record, and an audit of the questions that technical checks cannot settle. This project tests that combined method.

• Grounding: mathematical claims tied to the literature and external inputs identified at their exact Lean boundary.
• Technical verification: statement and axiom comparison, Landlock and network isolation, and replay through the Lean kernel and nanoda, as recorded in the Comparator note.
• Mathematical audit: source correspondence, definitions, hypotheses, concrete consumers, literature claims, and proof architecture tracked in the audit ledger.
• Traceability: declarations and transferred proof material connected to their sources by the provenance ledger.
• Exposition: mathematical arguments, implementation choices, and unresolved boundaries collected in these notes.

Together these layers let a reader follow a claim from the literature to its Lean declaration, downstream consumer, audit status, and executable check. The resulting draft includes the material a human needs to examine and digest the work.