You do not need to learn the project’s internal vocabulary first. Begin with the question you want to answer, then move into the exact theorem, source, or reproduction record.
Inspect the checked comparisons for completed nested supports and the counterexample to unrestricted local replacement. A smaller local replacement need not splice into the surrounding circuit without a cycle. The full source-derived admissibility and globally successful routing arguments remain open, alongside exact minimization and total polynomial bounds. The five global proof gates remain open.
Read the formal report guide →Inspect the compiled declaration inventory, theorem pins, axiom closures, source closure, and publication gate.
Inspect formal status →Check report identity, source coordinates, public payloads, and the clean-build commands.
Open the verification guide →Follow the path from Lean source to compiled inventory, publication map, status, report, and site.
Read plain-language milestone notes first, then open their source-derived technical details.
Read definitions of P, NP, Lean, machine checking, hashes, formal artefact coverage, and the separate risk-weighted proof-completion estimate.
External review is valuable audit evidence, but it is not a mathematical premise and does not activate publication.
Questions, counterexamples, proof gaps, source access, or reproduction support.
Vulnerabilities, compromised files, unsafe deployment behavior, or suspected artefact drift.
Topic or theorem: Exact source commit and tree: File, module, or declaration: Expected result: Observed result or counterexample: Commands and environment: Smallest reproducible evidence:
