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 route, the finite PkgC separating-consumer dichotomy, typed restoration realization, same-key cancellation, ambient-BN4-ledger embedding, theorem boundaries, reductions, missing global results, and five formal blockers.
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, and the progress 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:
