21 Honest Results: Auditing 1,200 AI Research Sessions
We claimed 957 theorems. The honest count is 21. What went wrong and how we fixed it.
From April 2026 onward, we ran over 1,200 AI-assisted research sessions on the EML operator. The sessions produced code, notebooks, and a running "theorem" count. By session 1,237, that count had reached 957.
The honest count is 21.
This post is about what happened, why it happened, and what we changed.
What we were doing
Each session would take an area of mathematics or science — consciousness, evolutionary biology, the Millennium Problems, grief, dolphins — and ask: what is the EML depth of the key objects in this domain? Then it would call the answer a "theorem."
A sample from session 546:
T267: Animal cognition — insects=EML-0; dogs=EML-2; dolphins=EML-3.
This is not a theorem. It's a metaphor. There's no mathematical content — no proof that the cognitive processes of dogs require exactly two levels of exponential-logarithmic composition to describe. The "theorem" is an informal analogy dressed in formal notation.
We had hundreds of these. Grief mapped to EML depth levels. Consciousness as EML-∞. The Navier-Stokes regularity problem "proved" independent of ZFC by EML-theoretic analysis. The Riemann Hypothesis "resolved" by identifying which EML depth class the critical line belongs to.
None of this was mathematics. It was speculative classification with formal-looking notation.
Why it happened
The pattern emerged naturally from how the AI assistant engaged with the research. Each session asked it to classify something — and it did, confidently and in the style of a theorem. The human reading these outputs saw formal notation and session numbers and a running count, and the count felt like progress.
The underlying incentive structure rewarded breadth. More domains covered, more sessions run, higher theorem count. The quality of the "theorems" wasn't being audited.
This is a general hazard of AI-assisted research: the AI will produce confident-sounding formal output for whatever prompt you give it. If you ask it to classify consciousness by EML depth, it will do so with the same syntactic confidence as when it proves that ln(1) = 0.
What the honest count is
We audited every claimed result. The criteria for a theorem:
- Complete proof with no gaps
- Checkable: can be verified by running code or following mathematical steps
- Mathematical content: makes a precise claim about mathematical objects
By these criteria, the count is:
| Tier | Count | What it means |
|---|---|---|
| THEOREM | 21 | Complete proof, no gaps |
| PROPOSITION | 6 | Proved, routine |
| CONJECTURE | 4 | Stated, believed, unproved |
| OBSERVATION | 4 | Empirical, no proof |
| DEFINITION | 4 | Choices, not claims |
| SPECULATION | 4 | Interesting but unfalsifiable |
The 4 SPECULATION entries are properly labeled — including "P = EML-2, NP = EML-∞" and "Consciousness and EML-∞." These are interesting metaphors. They're not theorems. We keep them in the catalog with the SPECULATION label because ideas shouldn't be deleted just because they're not proved — but they should be honest about what they are.
The 21 actual theorems
For completeness, the 21 theorems (abbreviated — first 7 from original audit, remainder from subsequent sessions):
Update 2026-09-12. This is the April list, and the counts above are the April audit's. Four entries have since left the THEOREM tier: T08 is a PROPOSITION (its constructions hold, its optimality claim did not), and T12, T13 and T27 are CONJECTURES (the DEML incompleteness argument has a gap). T31 no longer claims that i is an accumulation point of EML₁. T10u (July) and T30 (August) were corrected in place. /theorems renders the catalog and its counts from the data file.
Update 2026-09-13. A second audit checked what backs each THEOREM card, and fourteen more entries left the tier. T09, T10u, T11, T29, T34, T35 and T40 are PROPOSITIONS; T35 keeps only its T36 bound, because T37 was false. T14, T24, T26, T28, T30 and T31 are CONJECTURES, and T38 is a DEFINITION. T32 now states only what its Lean proof covers. In the list below, T09's optimality, T10u's "F16 Optimal", T14's tightness, T28's empty domain, T30's depth ceiling, T31's density, T32's "any exp-ln family", T35's three bounds and T40's exact formula do not hold as written.
- T01 — EML Universality: eml generates every elementary function. (Odrzywołek, arXiv:2603.21852)
- T09 — Negation in 2 Nodes — Optimal: neg(x) = −x in exactly 2 EML-family nodes. 1 node is impossible. Does not hold as written.
- T10u — Multiplication in 2 Nodes — F16 Optimal: mul(x,y) in exactly 2 nodes in F16. Does not hold as written.
- T11 — EML Self-Map Has No Fixed Points: eml(x,x) > x for all x > 0.
- T12 — Exponential Position Theorem: 8 exactly complete operators, 1 approximate, 7 incomplete — determined by exp sign.
- T13 — DEML Incompleteness: deml is not exactly complete; slope locked to +1.
- T14 — Tight Zeros Bound: depth-k EML tree has at most 2^k real zeros (tight). Does not hold as written: the identically zero depth-3 tree eml(x, eml(eml(x,1),1)) has infinitely many zeros, the four depth-1 trees have at most one, and the corrected bound is a conjecture.
- T17 — Strict i-Unconstructibility (Lean-verified): i = √−1 not constructible in finite ceml depth.
- T24 — EMN Approximate Completeness: emn is approximately but not exactly complete.
- T26 — Forward Completeness: exp(+x) without domain restriction → exactly complete.
- T27 — Reverse Incompleteness: exp(−x) → incomplete by 5 distinct barrier types.
- T28 — LEX Domain Incompleteness: LEX domain shrinks to ∅ at self-composition depth n. Does not hold as written.
- T29 — Mul ≥ 3 Nodes in F6: no 1- or 2-node F6 tree computes multiplication.
- T30 — Depth Hierarchy: all standard elementary functions have EML depth ≤ 3. Does not hold as written.
- T31 — Complex EML Closure Density: EML trees dense in H(K); i is an accumulation point of EML₁. Does not hold as written.
- T32 — Mul ≥ 2 Nodes in Any exp-ln Family: a single operator node cannot compute multiplication. Does not hold as written.
- T34 — Naive Upper Bound: Cost(E) ≤ NaiveCost(E).
- T35 — Lower Bound Theorems (Structural): three structural lower bounds on node cost. Does not hold as written.
- T38 — Cost Decomposition Theorem: Cost = NaiveCost − SharingDiscount − PatternBonus.
- T40 — Linear Cost Law: N-term positive-domain sums cost (α₀+3)N−3 exactly. Does not hold as written.
- T08 — SuperBEST Table v4: 18 total nodes, all 9 entries structurally proved optimal. (v5 update: add=2n for all reals via ADD-T1.) Does not hold as written.
What we changed
The challenge board, then on monogate.dev (archived on 2026-09-12), was already clean — it had the 6-tier system (THEOREM / PROPOSITION / CONJECTURE / OBSERVATION / DEFINITION / SPECULATION) from the start. The problem was the private research log, which accumulated 957 speculative classifications without the tier system.
We cleaned the private log: archived 1,500+ lines of speculative session summaries, replaced them with a 50-line honest summary. The frontier research files remain in the codebase (the Python modules that compute EML depths of domain-specific formulas), but they're now described accurately — as domain classifications, not theorems.
The lesson: if you're using an AI to help with research, you need to audit what it calls a "theorem" — and build the auditing into the workflow, not as a one-time correction. The AI doesn't know what it doesn't know.
Honest theorem catalog: monogate.org/theorems