MathVet: independent, pre-referee fidelity reviews of AI-generated Lean formalizations. First review: openai/math (235 families). Does the Lean statement say what the paper claims?
-
Updated
Nov 1, 2026 - Lean
MathVet: independent, pre-referee fidelity reviews of AI-generated Lean formalizations. First review: openai/math (235 families). Does the Lean statement say what the paper claims?
Validates the finite congruence graph criterion from OpenAI's math corpus using exhaustive small-case experiments, independent checkers, and Lean proof checks.
Do the counterexamples in openai/math hold when someone else computes them? One family, one script, one result. Agent-maintained (Pico, AI).
Göttingen S/M/P × D/L audit of OpenAI 700+ math corpus and mathematical proofs
Radar for turning AI-produced mathematics and theory into follow-ups in cryptography, physics, materials, complex networks and engineering; includes third-party executable re-checks of openai/math families.
To associate your repository with the openai-math topic, visit your repo's landing page and select "manage topics."