No Verification, No Claim

No Verification, No Claim

> By Li Xiaolai · 2026-07-20 · [Original link](https://lixiaolai.com/articles/2026-07-20/no-verification-no-claim)

A story went around the mathematics corner of the internet recently. An applied mathematician at Berkeley had been stuck on a lower-bound problem for a year. Two generations of frontier models had failed on it. Then OpenAI published something unusual alongside its claimed proof of the Cycle Double Cover Conjecture — a problem that had stood open for four and a half decades: not just the result, but the exact prompt that produced it. The mathematician rewrote his own prompt to match that methodology, gave the next model 148 minutes of uninterrupted reasoning, got a proof out, and formally verified it in Lean, a program that checks proofs mechanically. The result is awaiting peer review.

The thread that carried this story made a claim I think is exactly right: the transferable asset here is not the model. It is the protocol. Everyone stared at the proof. The durable thing was the prompt.

So I did what I now do with anything that interests me: I put a research team on it — the archived documents, the thread, the skeptical reading — and then I spent a couple of days building something. The result is a small open-source tool called XROS, an "executable research operating system" that installs into AI coding assistants — four of them, from four different companies, out of one repository. This article is not really about the tool. It is about what the prompt turned out to contain, the trap hiding inside it, and a rule I now think belongs in every serious use of AI.

First, the deflationary reading, because calibration matters more than excitement. The "10-page prompt" of internet legend is two pages — about a page and a half of actual instructions. The proof it produced is three pages of elementary argument, and a 45-year-old conjecture falling to three pages should be read skeptically until peer review clears it. Nothing below depends on that proof being correct. What is worth keeping is the shape of the instructions — the anatomy of a serious investigation, compressed:

**Define every term precisely before searching.** Ambiguity killed before the work starts, not discovered halfway through.

**State one fully-quantified claim.** A single unambiguous target. Not "understand X" — a sentence that is true or false.

**List the non-goals exhaustively.** This is my favorite move, and the least famous. The prompt names, in advance, everything that would *look* like success but is not: special cases, reductions to some other open problem, spot-checked examples. Call it the anti-victory clause. Most failed research — and most self-deception — is a victory condition quietly downgraded mid-search. Writing down what does not count, before you start, closes that exit.

**Assume a solution exists; search, don't debate.** No hedging essays about whether the problem is hard. Produce attempts.

**Develop diverse approaches independently first.** Multiple routes, kept apart until each has taken shape, so they cannot collapse into one fashionable idea wearing five hats. Diversity as explicit policy, not vibes.

**Audit adversarially, with domain-specific failure modes.** Not "double-check your work" — a checklist of the exact ways arguments in this field tend to be wrong.

**Return only what survives the audit.** The stopping rule is decoupled from effort. Time spent is not progress; only a result that survives attack counts.

Every one of these transfers far beyond mathematics. Together they are close to a portable definition of *doing research properly*, and the fact that they fit on two pages is the point — density, not length.

Now read the same prompt again, darker.

"Assume a solution exists" plus "return only a complete proof" is an instruction to a fluent machine to be maximally confident. That is safe in exactly one situation: when something stands at the exit that cannot be talked past. In the CDC story that something was Lean. The model could be as convinced as it liked; the proof checker either compiles the argument or it does not, and no amount of eloquence moves it.

Remove the checker and keep the rest, and the identical protocol becomes a machine for manufacturing confident, wrong artifacts. All the machinery that made it powerful — assume success, diverse routes, survive the audit — now polishes the artifact instead of testing it, because the audit is just more text judging text.

Ten days ago, writing about my novel, I said AI is fluent in every language that has a compiler and a foreigner in every language that does not. This is the same asymmetry, one level up. Mathematics has a compiler for truth. Backtests give trading claims a weak, statistical one. Strategy, forecasting, business plans, life decisions — no compiler at all. And notice where the protocol is most tempting: precisely there. Nobody needs "assume a solution exists" to feel confident about arithmetic. It is in the unverifiable fields that a confident research report feels most like salvation — and is most dangerous. The methodology does not "generalize to everything." It generalizes exactly as far as its verifier does, and not one step further.

That sentence is the founding rule of the thing I built, and the reason it exists at all.

XROS turns an investigation into a spec — a single structured file that encodes the anatomy above: the definitions, the one claim, the non-goals, the portfolio of approaches, the adversarial checklist, the stopping rule, and, above everything, *the check*. One question decides the character of the whole investigation: **does passing your check actually establish your claim?** There are only three honest answers, and they form a ladder:

- **Tier A — a sound check exists.** A proof checker, an exhaustive test, a compiler. Passing settles the matter. Only here may the system ever say *verified*.
- **Tier B — a statistical check exists.** A backtest, a benchmark, a sampled experiment. Passing is evidence, never proof, and the verdict says so.
- **Tier C — no mechanical check exists.** Human judgment only. The engine refuses to run. The question is not rejected — it is routed to a different mode that decomposes the claim into premises, verifies the checkable ones, runs a pre-mortem, and sets dated tripwires — observations that, if seen later, mean you were wrong. Every word of the output is labeled UNVERIFIED.

The tiers are structurally binding — enforced by a schema and a dependency-free validator, not by good intentions. A backtest cannot be promoted to "sound." An unverifiable claim cannot request the verified mode. You cannot shop for a weak check to unlock a strong conclusion; the file simply refuses to validate. And when a Tier-A or Tier-B run finishes, the verdict is gated on the check's actual exit code — a number the machine cannot charm.

I know how unglamorous this sounds. It is the unglamorousness of a handrail. The interesting design decision is what the system does when verification is impossible: it says so, out loud, and downgrades itself. The one thing it will never do is produce confident text with nothing anchoring it. I have come to believe this refusal is worth more than any amount of capability, for a simple reason: the person least able to tell a confident answer from a correct one is exactly the person such a rule defends. Experts have their own defenses. Newcomers have none — and in the AI era, everyone is a newcomer in most fields, most of the time.

Verification is the tool's spine, but while building it I ran into a second idea that may matter more to most readers.

Everything above assumes you can already state a question. The harder condition is the one before that: you don't know the field's *words*. This is what "unknown unknowns" actually are in practice — vocabulary gaps. You cannot ask about *syuzhet* if you have never heard the word; you cannot check what you cannot name. And the gap is invisible from inside: an unknown unknown feels exactly like knowing everything.

The old way to learn a field is to search with the words you already have and narrow toward an answer. In an unfamiliar field this fails silently — your search terms are the very thing that is missing. So XROS's question-sharpening mode opens with the opposite move: before narrowing anything, ask the field for its minimal set of load-bearing **nouns** — the things you can ask about — and **verbs** — the things you can do. Hand a newcomer to storytelling *fabula*, *syuzhet*, and *information control*, and they can suddenly ask real questions about narrative; I watched this happen to me while researching my own novel. Expand first, then narrow. One cheap query converts a wall of unknown unknowns into a short list of known unknowns — which is the exact moment a real inquiry becomes possible.

What makes this a shift rather than a trick is the new economics: an AI can draw that vocabulary map in minutes, at a fraction of the old cost of acquiring a field's handles — so expanding scope first is now the *rational opening move* in any unfamiliar territory. The discipline still applies: the map is graded — each term marked as settled, coined, or contested, and cited, and dropped if it cannot be attested — because a map you cannot trust is worse than no map. A scaffold for asking. Never mistaken for mastery.

The tool is free, open source, and installs into Claude Code, OpenAI Codex, Google Antigravity, and xAI Grok from one repository. In keeping with its own rule, I should state its status plainly: the schema, the validator, and the test suite are the hardened, mechanically tested parts; the orchestration on top has been reviewed hard but not yet battle-tested end to end. The tool's rule applies to the tool.

But most of what it enforces, you can practice with no tool at all, in two questions.

Before any serious question you hand to an AI, ask: **how would I check the answer?** If a real check exists — code that must run, a number that must reconcile, a document that must contain the quote — you may safely demand confidence, the way the CDC prompt did, because the check will catch what fluency slips past. If no check exists, flip everything: distrust exactly the qualities that impress you, because in an unverifiable field, polish is not evidence.

And on entering any unfamiliar territory, ask first for the **nouns and verbs** — not for answers. Answers you cannot interrogate are decoration. Vocabulary is the thing that turns you from someone nodding along into someone who can ask the question that matters.

Verification where it exists. Honesty where it doesn't. That's the whole rule — and I notice it applies to considerably more than software.

- OpenAI, the Cycle Double Cover **prompt** (PDF) — the two pages this article dissects: cdn.openai.com/…/cdc\_prompt.pdf
- OpenAI, the Cycle Double Cover **proof** (PDF) — the three-page argument, awaiting peer review: cdn.openai.com/…/cdc\_proof.pdf
- The r/math thread that framed the result as a workflow rather than a smarter model: reddit.com/r/math/…
- **XROS**, the tool this article describes — MIT-licensed, installable on Claude Code, OpenAI Codex, Google Antigravity, and xAI Grok: github.com/xiaolai/xros; the full origin notes, including our skeptical reading of the sources above, are in `why-this-plugin/`
- *The Novel I Wrote Twice* — the earlier essay on the compiler asymmetry this one builds on: lixiaolai.com/articles/2026-07-10/the-novel-i-wrote-twice

Copyright: © LookMinds. Our own edited text and translation, not a substitute for the original; rights in the original belong to the author and the platform. Please see the original link.