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

2026-11-03来源 dev.to AIEnglish

Recently, OpenAI released a repository of formal proofs (ten-proofs) demonstrating AI's capability to solve complex mathematical problems using Lean 4.

When an AI lab drops thousands of lines of formal code claiming "we solved it," how does the rest of the world verify it? Currently, we rely on a handful of expert mathematicians who don't have the time to read 37,000 lines of code. Or, we rely on another LLM to "judge" it—which just hallucinates a thumbs-up.

I wanted to see if an automated, physical-witness approach could do better. So, I used my open-source project, harness-audit-sidecar, to audit OpenAI's proofs locally.

Here is what happened.

The Setup: No Hallucinations Allowed

LLM-as-a-Judge fails here. A compiler asks "does this elaborate?", but an auditor must ask "is there a physical witness?".

To create a physical witness, I didn't just scan the text. I pulled the 7.2 GB Mathlib cache, compiled 8,687 jobs locally, and ran our LeanProofAuditor.

The Results: 11 PASS, 12 FAIL

The audit took about 40 minutes. Here are the hard facts:

  1. The 11 Main Proof Files achieved a genuine PASS.
    All theorems elaborated successfully. Zero smuggled custom axioms. They rely only on the three standard Lean axioms (Classical.choice, propext, Quot.sound). OpenAI's core mathematical proofs are solid.

  2. 12 Files returned FAIL (42 placeholders found).
    Wait, did OpenAI cheat? No. These 12 files are located in ComparatorChallenges/. They are templates intentionally left with sorry (Lean's unproved placeholder) for human contestants to fill out. Our auditor simply reported the physical fact: these files are not complete proofs.

Why This Matters

If an LLM judged this repository, it would read the comments, see the word "solved", and output a confident PASS for the whole folder—completely ignoring the 42 sorry placeholders.

Our sidecar enforces a four-valued verdict: PASS, FAIL, INVALID, NOT RUN.

  • It didn't just guess.
  • It didn't accept exit code 0 as proof (because a file with sorry can compile cleanly).
  • It inspected the artifact's dependency graph via #print axioms to expose the truth.

The Four-Valued Immune System

This audit is just one application of the harness-audit-sidecar. Originally, it was built to catch AI agents lying about writing files or executing shell commands.

We introduced:

  • Conditional Immunity: Tier 1 (cheap stat checks) and Tier 2 (full Git diffs). Two consecutive FAILs trigger an "inflammation storm" that blocks writes.
  • Membrane Gateway: Agents cannot define their own success criteria. They must register expectations before execution.
  • Agent Metabolism OS: Regulates LLM API costs and fast/slow thinking beats.

A Tool that Audits Itself

During development, our own auditor caught itself producing false completions. We log these in ERRATA.md. For example, we initially failed a legitimate opaque definition because we confused it with an axiom. We corrected it and wrote a regression test.

An audit tool that only audits others is a decoration. You can read our ERRATA to see how the system caught its own bugs.

Resources:

原文：https://www.a8q9.cn/en/article/trust-but-verify-how-we-audited-openai-s-lean-4-math-proofs-with-a-zero-dependen-f0ddff.html

相关文章