lean-generated-proof-audit

Check whether a machine-generated Lean 4 proof actually proves its theorem. A proof can appear in the environment, pass lake build, and still not have been proved: when elaboration fails Lean admits the declaration carrying sorryAx, which an axiom report cannot tell apart from a sorry somebody typed. Use when auditing output from a prover or an LLM, scoring a proof benchmark, asking whether an AI-written proof is…