Proof Audit

Assess the actual argument against the exact theorem. Read enough of the proof and its dependencies to reconstruct the decisive step. Preserve the difference between a proof defect and a publication or verification boundary.

Focus the challenge

• Recover the statement, definitions, hypotheses, quantifiers, and conclusion. Check that reductions preserve them and do not silently restrict the problem.
• Identify the load-bearing inference. Derive it independently or supply a concrete obstruction. Check equivalent-conjecture assumptions, sign and normalization errors, missing domains, boundary cases, multiplicities, and the interchange of limits, sums, or derivatives when relevant.
• For uniform estimates, track every constant and parameter. For operators, check the actual domain and whether the claimed selfadjointness is proved. For a finite computation, check error bounds and what is certified beyond sample points.
• Give each substantive finding an exact location, the failed implication, and a counterexample or repair obligation. Vague unease, lack of peer review, and lack of Lean formalization are not mathematical findings.
• Distinguish false statements from arguments that have not established a true statement. A stronger hypothesis or a restricted conclusion can be a useful repair, but must be labeled as a changed theorem.

Use a fresh-context agent for a complex independent reconstruction when delegation is available and permitted. Supply the statement and raw proof, not the preferred conclusion. Do not require different model brands or claim that independent agents are independent mathematical authorities.

Verdict

Report the exact checked range and one of:

• Proof established in the checked scope: a complete argument has been reconstructed and no substantive gap remains in that range. Say which hypotheses apply and what can now be used.
• Candidate with a specific gap: identify the inference still requiring proof and its consequences for the claim.
• Claim refuted as stated: provide the contradiction or counterexample and a possible restricted replacement.

Do not claim the entire manuscript has been checked when only a bridge lemma was inspected. A passing compiler, checksum, wording test, or agent vote is not proof verification. An accepted lemma can be used immediately; reopen it only for a concrete new reason.

Use the audit template when delegating or drafting an audit prompt. If repairs are not requested, return findings without changing the manuscript.

For a supplied Lean artifact or a requested formal-verification claim, use lean-verification to compare the actual target and its transitive dependencies. Lack of formalization alone remains distinct from a substantive proof defect.