Trust, but verify, audit and attribute: a human-in-the-loop framework for checking AI-produced research results
György Eigner, Patrik P. Süli, Roland Hollós
cs.AI
Nov 9, 2026 · v1
cs.CY cs.HC cs.LO
TL;DR
Lean 4 with Mathlib, called through the lean-lsp MCP server, is the formal-proof tool in an agentic math-checking toolchain alongside Wolfram Language and MATLAB.
Abstract
Artificial intelligence (AI) systems now produce research results in bulk: in October 2026 a single laboratory released more than 700 AI-generated mathematics manuscripts, only part of them with machine-checked proofs. Such volumes will be checked mostly by AI agents that call specialised software. A passing check certifies only the artefact that was checked. For proofs translated into the proof assistant Lean, it has been shown that this artefact may state something other than the author's text, and that deciding whether a translation is faithful is undecidable in general. The human researcher therefore stays in the loop, and human and AI contributions must be recorded. We propose a domain-independent, human-in-the-loop framework for checking AI-produced results. Validated, agent-usable tools with different grounds of trust check the results; a fidelity audit asks whether each check addressed the claim as stated; the human decides at fixed points; and a dialog report attributes the work to the human and to the AI. We describe two automatic implementations of the tool layer, for mathematics (Wolfram Language, MATLAB, Lean) and statistics (Python and R), and run the mathematical one on a two-claim example. An ambiguous claim was split into two readings, one refuted and one proved.
Problem
AI systems now produce research results in volume, and those results are increasingly checked by AI agents calling software such as Lean. A passing check certifies only the artefact checked, which may not faithfully state the author's claim. For Lean translations, whether a translation is faithful is undecidable in general.
Approach
The authors propose a domain-independent human-in-the-loop framework. Validated tools with different grounds of trust check the results. A fidelity audit then asks whether each check addressed the claim as stated, using frozen targets, forbidden acts and a deviation protocol. Humans decide at four fixed points, and a dialog report attributes contributions to the human and the AI. Two agent-skill implementations are described: math-prove-tool (Wolfram Language, MATLAB, Lean 4 + Mathlib via MCP) and stat-prove-tool (Python and R).
Results
math-prove-tool was run on two claims. The divisibility claim was confirmed by all three tools. The ambiguous maximum-value claim was split into two readings: Wolfram and Lean refuted the exact reading and confirmed the rounded one, while MATLAB was inconclusive on both.
| Claim | Wolfram Language | MATLAB | Lean | Agreement |
|---|
| P01 | general proof, confirmed | general proof, confirmed (back-translation partial) | general proof, confirmed | agree |
| P02a | general proof, refuted | symbolic instance, inconclusive | general proof, refuted | partial |
| P02b | general proof, confirmed | symbolic instance, inconclusive | general proof, confirmed | partial |
Results of the example run per claim and tool