ProofNetVerif

ProofNetVerif is an evaluation benchmark comprising 3,752 entries, each including an informal mathematical statement, its reference formalization, a predicted formalization, and a binary label indicating semantic equivalence. It is designed to assess autoformalization metrics by providing a challenging testbed for both reference-based and reference-free evaluation approaches.