Trust, but Verify: How We Audited OpenAI's Lean 4 Math Proofs with a Zero-Dependency Sidecar

Recently, OpenAI released a repository of formal proofs (ten-proofs) demonstrating AI's capability to...