Cases
Case studies
What we checked, how, and what we could not check, in two mathematical-physics papers our founder wrote with AI agents (arXiv:2610.34122, arXiv:2610.34125; under review at a journal). All the records are public.
1. The paper's constants, checked in Lean without floating point
The main result of Paper II contains the constants 0.3441, 0.2985 and 0.1252. We proved the corresponding inequalities in Lean 4 / Mathlib from series bounds for the logarithm and for π, without floating-point arithmetic and without native_decide.
In all, 23 computations from the proofs of Papers I and II are formalized. Six of them take the form "if the paper's analytic result holds, the conclusion follows"; the hypothesis itself is not checked in Lean.
Not verified: the main theorems themselves (Fock space, the Hamiltonian and operator spectra do not appear in Lean). See "What is NOT verified" in the formalization repository.
2. A lemma that passed every audit still had a gap
Lemma 8.2 of Paper II passed independent audit layers, a "no gaps" verdict from a second AI, and the author's own reading, and went onto arXiv. Later, yet another AI acting as a referee pointed out a gap. Auditing that report showed the gap was real, but the claim was not false and could be repaired.
The lesson: you cannot say "there are certainly no gaps". You can only say you did what you could to remove them, and closed every gap that was found. That is why our reports always list what was checked next to what was not.
3. 452 failures, written down
From 2 September to 22 October 2026 we logged 452 abandoned approaches, disproved hopes and failed computations. Each entry records what was closed — a method, a target, or the truth of a statement — so the same dead end was not walked twice. The log also shows that failures declared "impossible in principle" were overturned by later audits more than once.
Full index of failures (in Japanese)
4. Another AI's "fully verified" was checked one by one
To simplify the proofs, we took 52 proposals from a different AI and audited each one. Some contained real ideas and made a paper lighter. But of the three marked "fully verified", one was wrong, and two delivered about a tenth of the claimed effect. An AI's own "verified" is not a substitute for verification.
5. Scored by readers with different roles
We gave AI readers three roles — operator-theory rigor, referee, and simplification — and revised until all six readers of the two papers scored above 4.5 out of 5. First scores of 3.9–4.2 rose to 4.6–4.7. This does not replace external peer review; it adds readers before submission.
The same method, on your problem
We can set up the same rules and tools for your own research. Start with a fixed-price two-week pilot.