What does this research mean for the field?

A human-directed, two-model formalization loop incorporating continuous axiom-budget auditing and adversarial review effectively identifies structural and semantic faults in AI-generated mathematical proofs, ensuring trustworthy formalization without hidden or false assumptions. Novelty: ClaimNovelty.METHODOLOGICAL. Consensus alignment: ConsensusAlignment.NEUTRAL.

What question did this study set out to answer?

The aim is to develop a robust human-directed feedback loop for auditing AI-generated mathematics and coding to improve trustworthiness.

June 27, 2026Open Access

An Audited Human-AI Loop for Trustworthy Lean Formalization: Axiom-Budget Auditing, a Goal-Directed State Report, and a Conditional General-Relativity Case Study

Key Points

The aim is to develop a robust human-directed feedback loop for auditing AI-generated mathematics and coding to improve trustworthiness.
Implemented a two-model formalization loop with a coding agent and an independent adversarial model.
Introduced an axiom budget for auditing and classifying results as proved, conditional, or cited.
Conducted a controlled instrument ablation to assess structural fault detection by various components.
Achieved successful diagnosis of semantic faults, distinguishing between false axioms and circular hypotheses.
Demonstrated a project-axiom-free Lean theorem that conditionally derives the Einstein field equations.
Verification confirmed the absence of hidden axioms, ensuring the transparency of formal claims.

Abstract

AI can now write mathematics and code faster than humans can vet it, and in a proof assistant a proof that merely compiles is not enough: the load-bearing content can hide in a declared axiom, and "it builds, with no sorry" cannot distinguish a sound development from one resting on a false, vacuous, or over-strong assumption. This paper presents a human-directed, two-model formalization loop built around that gap. A coding agent (Claude Code) writes Lean 4 / Mathlib and self-corrects against the compiler; an independent model (GPT-5.5-Pro) adversarially reviews the design rather than the syntax; and a human controls scope and premises. The soundness contribution is the audit that wraps the loop: a continuously-enforced axiom budget that classifies every result as proved/conditional/cited and can only ratchet down; a vacuity lint and a hypothesis ledger / redundancy probe that extend the audit from declared axioms to a theorem's local hypotheses; a goal-directed track-state report that turns the audit into the loop's steering signal; and a link-checked blueprint from prose to kernel-checked declarations. A small controlled instrument ablation shows that the structural instruments catch structural faults while only the independent reviewer diagnoses the semantic ones (a false-but-well-typed axiom, a circular hypothesis). As a demanding case study, the loop is driven to a machine-checked, project-axiom-free Lean theorem that derives, conditionally, the Einstein field equations from a finite-information capacity bound by a Jacobson-style equation of state, with the cited physics inputs carried as explicit, labelled hypotheses and a machine-checked witness that the premise set is jointly satisfiable. The case study stresses the workflow, not physics: verification certifies the conditional mathematics and the absence of any hidden axiom; it does not establish the cited inputs or the framework's physical postulates, which remain open.

Read Full Paperexternally

Ask AI

Helpful

Bookmark

View Full Paper