Logical equivalence is too permissive a test of whether a formal statement faithfully matches its reference, because a strong prover can connect any two provable statements through P ↔ True ↔ Q. SemantEq is a finer relation under which each statement must turn into the other by meaning-preserving steps alone, such as logical rearrangement and rewriting with the library's own equations, and a proof is judged by the term Lean checks rather than by its tactic script. SemantEq-Eval searches for such chains with no model and reaches 100% precision on ProofNetVerif. SemantEq-ProofAudit holds proofs written by a language model to the same standard, accepting none of the non-equivalent pairs while raising recall from 65% to 81%.

Infrastructure for LLM-based theorem proving that spans Lean, Coq, and Isabelle, so that the same prover, data pipeline, and evaluation can be used across proof assistants instead of being rebuilt for each one.