Lean Verification

Check what the supplied Lean artifact proves, and whether it proves the mathematical statement the user asked about. Positive conclusions should be stated directly with their exact scope; compilation, agent agreement, and external acceptance are distinct evidence.

Check the target, then its proof

1. Recover the intended statement independently of the candidate implementation. Compare definitions, quantifiers, hypotheses, implicit arguments, instances, and the elaborated target type. A proof of an implication assuming the desired conclusion is not a proof of the original theorem.
2. Identify the actual project, compiler version, dependencies, source revision, and target declaration. Use the pinned project environment. Inspect supplied build configuration and imports before executing unfamiliar code. Reuse relevant successful evidence for unchanged artifacts; rebuild when the target or its dependencies changed or the evidence does not cover them.
3. Run the narrow relevant Lean/Lake check and inspect warnings as well as exit status. If tools are missing, report the source assessment and the exact unexecuted command; do not invent compilation evidence or install dependencies automatically.
4. Inspect #print axioms TargetDeclaration for the target and its transitive dependencies. sorryAx means incomplete proof. Custom axioms require an explicit justification or a conditional verdict. Accept the standard logical axioms propext, Classical.choice, and Quot.sound without mislabeling them as mathematical gaps. Native-evaluation or compiler-trust dependencies require a clearly stated trust boundary appropriate to the installed version.
5. Check meaningful remaining risks: notation or definitions that change the statement, unchecked declarations or kernel-bypass settings, and unsupported claims about a whole project based on one checked declaration. Choose further replay or external checking only when the task and risk justify it, using Lean assurance.

A textual search for sorry helps locate unfinished work but does not replace the transitive dependency check. A source tree containing an unrelated unfinished theorem does not make a target that has a complete, checked dependency closure incomplete.

State a usable verdict

• Formally verified in the stated environment: the actual target matches the intended statement, relevant checks succeeded, and its dependency closure has no unfinished or unsupported mathematical assumptions. Name the check and any disclosed trust extensions.
• Formally conditional or incomplete: specify the assumed axiom, missing goal, statement mismatch, or unavailable execution evidence. A successful build with sorryAx cannot receive a complete verdict.
• Candidate rejected: give the concrete contradiction, mismatch, or failed check and a repair obligation.

Separate an analytical proof's established status from its formalization status. A lack of Lean tooling or library support is not an analytical refutation. A genuine logical defect is. Separate correctness, originality, and publication acceptance as well.

Use the verification report for a compact record. When a repair is authorized, repair the responsible statement or proof and repeat only the affected checks. On pause, preserve evidence and the exact next obligation without starting new work.