于是我做了我现在对任何让我感兴趣的东西都会做的事：我派出一个研究团队——档案文档、thread、怀疑性阅读——然后花了几天时间做了点东西。结果是一个小型开源工具，叫 XROS，一个“可执行研究操作系统”，可以从同一个仓库安装进四家不同公司的 AI 编程助手。这篇文章其实并不是讲这个工具。它讲的是：那段提示词里究竟藏着什么，里面潜伏着什么陷阱，以及一条我现在认为每一次严肃使用 AI 都应遵守的规则。
十天前，写我的小说时，我说 AI 在每一种有编译器的语言里都很流利，在每一种没有编译器的语言里都是外国人。这是同一种不对称，只是上升了一层。数学有一个面向真理的编译器。回测给交易主张提供了一个弱的、统计性的编译器。战略、预测、商业计划、人生决策——完全没有编译器。注意这个协议最诱人的地方恰恰在哪里：正是在这些地方。没有人需要靠“假设解存在”来对算术产生信心。正是在那些不可验证的领域里，一份自信的研究报告最像救赎——也最危险。这套方法并不会“泛化到一切”。它只会刚好泛化到验证器所能抵达的地方，再往前一步都不行。
我知道这听起来一点也不迷人。它就是扶手那种不迷人。真正有意思的设计决定，是系统在无法验证时做什么：它会大声说出来，并且自我降级。它唯一绝不会做的事，是在没有任何锚点时产出自信文本。我越来越相信，这种拒绝比任何能力都更值钱，理由很简单：最不能分辨“自信答案”和“正确答案”的人，恰恰就是这条规则要保护的人。专家有自己的防线。新手没有——而在 AI 时代，大多数领域里，大多数时候，我们每个人都是新手。
学习一个领域的老办法，是用你已经拥有的词去搜索，然后不断收窄，靠近一个答案。在陌生领域里，这种方法会静悄悄地失败——因为你缺的恰恰就是搜索词。所以，XROS 的问题锐化模式一开始做相反的事：在收窄任何东西之前，先向这个领域索取一组最小的承重名词——你可以提问的那些东西——以及承重动词——你可以做的那些动作。把 fabula、syuzhet 和 information control 交给一个讲故事的新手，他就突然能对叙事提出真正的问题；我在研究自己的小说时，就亲眼看见这件事发生在自己身上。先扩展，再收窄。一次便宜的查询，就能把一堵未知的未知之墙，转成一小列已知的未知——而那正是真正的探究终于变得可能的时刻。
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.
"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 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/
