ProofGate: A Reproducible Audit of Faithfulness, Alignment, and Vacuity in State-of-the-Art Lean Theorem Provers

Recent neural theorem provers report pass rates on miniF2F and PutnamBench that, taken at face value, suggest formal mathematical reasoning is nearly solved. We argue that the reported figures conflate three distinct phenomena—proof faithfulness, statement alignment, and problem vacuity—and that a single failed check in any one can render a reported result an unaudited claim. We propose ProofGate, a reproducible audit pipeline implementing four orthogonal checks (kernel-level axiom inspection, banned-tactic linter, negation-counterexample probe, FormalAlign-style alignment score) that together yield a single dimensionless metric, Faithful-Pass. We release ProofGate as a Python package and apply it to every publicly released proof artifact of three recent state-of-the-art systems. Three findings are particularly noteworthy. First, the full kernel-level audit of all 635 DeepSeek-Prover-V2 (miniF2F-test and -valid combined) and Kimina-Prover-72B miniF2F-test proofs against each prover's pinned mathlib revision yields Kernel-Faithful-Pass$_{\mathcal{T}_1}$ = 100%, with no occurrences of `sorry` and no extra axioms beyond the compiler-trust set; under the strict trusted base $\mathcal{T}_0$, all 438 DeepSeek proofs pass while 186/197 Kimina proofs pass, the eleven exceptions being precisely those that invoke `native_decide`. Second, SBERT-based alignment scoring on the same items returns a 15.2% misalignment rate on DeepSeek miniF2F-test, within 1.2 percentage points of ReForm's expert-annotated rate. Third, Goedel-Prover-V2's "released proofs" for miniF2F are in fact the benchmark input statements with `sorry` placeholders; the public release contains no auditable proofs, a property the accompanying paper does not state explicitly.