没有验证，就没有结论

作者：李笑来 · 来源：lixiaolai.com · 发布于 2026-07-20 · 原文链接

最近，数学互联网的一角流传着一个故事。伯克利的一位应用数学家，在一个 lower-bound 问题上卡了一年。两代前沿模型都没能解决它。随后，OpenAI 在宣布自己给出 Cycle Double Cover Conjecture 的证明时，附带发布了一件不寻常的东西——这个问题已经悬而未决四十五年半；OpenAI 不只发布了结果，还发布了产生这个结果…

图 1：一段自信的研究结论被红色印章划掉，印章写着 UNVERIFIED, NO CHECK WAS RUN。

最近，数学互联网的一角流传着一个故事。伯克利的一位应用数学家，在一个 lower-bound 问题上卡了一年。两代前沿模型都没能解决它。随后，OpenAI 在宣布自己给出 Cycle Double Cover Conjecture 的证明时，附带发布了一件不寻常的东西——这个问题已经悬而未决四十五年半；OpenAI 不只发布了结果，还发布了产生这个结果的完整提示词。那位数学家把自己的提示词改写成同样的方法，让下一代模型连续推理 148 分钟，得到了一个证明，并用 Lean 正式验证了它。Lean 是一个会机械检查证明的程序。这个结果目前还在等待同行评审。

传播这个故事的 thread 提出了一个我认为完全正确的说法：这里真正可迁移的资产不是模型。是协议。所有人都盯着那个证明看。真正耐久的东西，是那段提示词。

于是我做了我现在对任何让我感兴趣的东西都会做的事：我派出一个研究团队——档案文档、thread、怀疑性阅读——然后花了几天时间做了点东西。结果是一个小型开源工具，叫 XROS，一个“可执行研究操作系统”，可以从同一个仓库安装进四家不同公司的 AI 编程助手。这篇文章其实并不是讲这个工具。它讲的是：那段提示词里究竟藏着什么，里面潜伏着什么陷阱，以及一条我现在认为每一次严肃使用 AI 都应遵守的规则。

提示词里实际包含什么#

先说一个降温版解读，因为校准比兴奋更重要。互联网传说中的“十页提示词”，其实只有两页——真正的指令大约一页半。它生成的证明，是三页初等论证；一个四十五年的 conjecture 被三页纸解决，在同行评审通过之前，都应该带着怀疑去读。下面的内容不依赖那个证明是否正确。值得留下的是这些指令的形状——一场严肃调查的解剖结构，被压缩在一起：

搜索之前，先精确定义每个术语。 模糊性在工作开始前就被杀掉，而不是做到一半才被发现。

陈述一个完全量化的主张。 一个单一、清楚的目标。不是“理解 X”，而是一个可以判真假的句子。

穷尽列出非目标。 这是我最喜欢的一招，也是最不出名的一招。提示词提前命名了所有那些_看起来_像成功、但并不算成功的东西：特殊情形、把问题化约到另一个开放问题、抽查过几个例子。不妨把它叫作反胜利条款。大多数失败的研究——也包括大多数自我欺骗——都是搜索进行到一半时，胜利条件被悄悄降级。开始前就写下什么不算，等于堵住了这个出口。

假设解存在；去搜索，不要辩论。 不要写一篇对冲式短文，讨论这个问题是不是很难。给出尝试。

先独立发展多条不同路线。 多条路径，在各自成形之前彼此隔离，这样它们才不会坍缩成同一个流行想法，只是戴了五顶帽子。多样性是明文政策，不是感觉。

以对抗方式审计，并使用领域特定的失败模式。 不是“再检查一下你的工作”，而是列出这个领域里的论证最常出错的具体方式。

只返回经得住审计的东西。 停止规则与投入努力脱钩。花了多少时间不等于进展；只有经得住攻击的结果才算数。

这些动作中的每一个，都远远超出数学领域。放在一起，它们几乎就是一个可迁移的“如何正确做研究”的定义。而它们能放进两页纸，正是重点所在——重要的是密度，不是长度。

陷阱#

现在，换一种更暗的方式，再读一遍同一段提示词。

“假设解存在”加上“只返回完整证明”，等于要求一台流利的机器最大限度地自信。这只在一种情况下安全：出口处站着某个无法被言辞绕过去的东西。在 CDC 的故事里，那个东西是 Lean。模型可以爱怎么确信就怎么确信；证明检查器要么编译这个论证，要么不编译。再多雄辩也打动不了它。

拿掉检查器，保留其余部分，同一个协议就会变成一台制造自信错误成果的机器。让它强大的所有机制——假设成功、多条路线、通过审计——现在都会去打磨成果，而不是测试成果，因为审计也只是更多文本在评判文本。

十天前，写我的小说时，我说 AI 在每一种有编译器的语言里都很流利，在每一种没有编译器的语言里都是外国人。这是同一种不对称，只是上升了一层。数学有一个面向真理的编译器。回测给交易主张提供了一个弱的、统计性的编译器。战略、预测、商业计划、人生决策——完全没有编译器。注意这个协议最诱人的地方恰恰在哪里：正是在这些地方。没有人需要靠“假设解存在”来对算术产生信心。正是在那些不可验证的领域里，一份自信的研究报告最像救赎——也最危险。这套方法并不会“泛化到一切”。它只会刚好泛化到验证器所能抵达的地方，再往前一步都不行。

没有验证，就没有结论#

这句话，是我做的那个东西的创始规则，也是它之所以存在的原因。

XROS 把一次调查变成一份 spec——一个结构化文件，编码上面那套解剖结构：定义、那个唯一主张、非目标、方法组合、对抗性检查清单、停止规则，以及最重要的，检查。有一个问题决定整场调查的性质：​通过你的检查，是否真的足以建立你的主张？ 诚实的答案只有三种，它们构成一架梯子：

  • Tier A——存在可靠检查。 证明检查器、穷尽测试、编译器。通过就能定案。只有在这里，系统才可以说 verified。
  • Tier B——存在统计性检查。 回测、benchmark、抽样实验。通过意味着证据，从来不意味着证明，结论必须明说这一点。
  • Tier C——不存在机械检查。 只有人类判断。引擎拒绝运行。问题并没有被拒绝——它被路由到另一种模式：拆解主张中的前提，验证其中可检查的部分，做一次预演失败，并设置带日期的触发线——如果未来观察到这些信号，就说明你错了。输出中的每个字都标记为 UNVERIFIED。

这些层级是结构性约束——由 schema 和一个无依赖 validator 强制执行，不靠良好意愿。回测不能被提升为“可靠”。不可验证的主张不能请求 verified 模式。你不能挑一个弱检查来解锁一个强结论；这个文件会直接拒绝通过验证。当 Tier-A 或 Tier-B 运行结束时，结论还会被检查的真实退出码卡住——那是一个机器无法用漂亮话打动的数字。

我知道这听起来一点也不迷人。它就是扶手那种不迷人。真正有意思的设计决定，是系统在无法验证时做什么：它会大声说出来，并且自我降级。它唯一绝不会做的事，是在没有任何锚点时产出自信文本。我越来越相信，这种拒绝比任何能力都更值钱，理由很简单：最不能分辨“自信答案”和“正确答案”的人，恰恰就是这条规则要保护的人。专家有自己的防线。新手没有——而在 AI 时代，大多数领域里，大多数时候，我们每个人都是新手。

另一半：先向未知扩展#

验证是这个工具的脊柱，但在构建它的过程中，我碰到了第二个想法；对大多数读者来说，它可能更重要。

上面的一切，都假设你已经能够提出一个问题。更难的状态在那之前：你不知道这个领域的_词_。所谓“未知的未知”，在实践中其实就是词汇缺口。你从没听过 syuzhet 这个词，就不可能问关于 syuzhet 的问题；你叫不出名字的东西，也就无法检查。而且这个缺口从内部看不见：一个未知的未知，感觉起来和“我什么都知道”一模一样。

学习一个领域的老办法，是用你已经拥有的词去搜索，然后不断收窄，靠近一个答案。在陌生领域里，这种方法会静悄悄地失败——因为你缺的恰恰就是搜索词。所以，XROS 的问题锐化模式一开始做相反的事：在收窄任何东西之前，先向这个领域索取一组最小的承重名词​——你可以提问的那些东西——以及承重动词​——你可以做的那些动作。把 fabula、syuzhet 和 information control 交给一个讲故事的新手，他就突然能对叙事提出真正的问题；我在研究自己的小说时，就亲眼看见这件事发生在自己身上。先扩展，再收窄。一次便宜的查询，就能把一堵未知的未知之墙，转成一小列已知的未知——而那正是真正的探究终于变得可能的时刻。

这之所以是一次转变，而不只是一个技巧，是因为新的经济性：AI 可以在几分钟内画出那张词汇地图，成本只是过去获取一个领域把手的一小部分。因此，在任何陌生地带，先扩展范围已经成了_理性的开场动作_。纪律仍然适用：这张地图要分级——每个术语都标明是 settled、coined 还是 contested，要有引用，无法证实就丢掉——因为一张不能信任的地图，比没有地图更糟。它是一副用来提问的脚手架。绝不能误认为已经掌握。

不用工具，也能养成的习惯#

这个工具是免费的、开源的，可以从一个仓库安装进 Claude Code、OpenAI Codex、Google Antigravity 和 xAI Grok。按它自己的规则，我应该直说它现在的状态：schema、validator 和测试套件，是已经硬化、经过机械测试的部分；上层编排经过了严格审阅，但还没有端到端地经历实战考验。这个工具的规则，同样适用于这个工具本身。

不过，它强制执行的大多数东西，不用任何工具也能练，只需要两个问题。

在把任何严肃问题交给 AI 之前，先问：​我将如何检查这个答案？ 如果存在真实检查——必须运行的代码、必须对得上的数字、必须包含引文的文档——你就可以像 CDC prompt 那样安全地要求信心，因为检查会抓住流利语言滑过去的东西。如果不存在检查，就把一切反过来：越是让你印象深刻的特质，越要怀疑；因为在不可验证的领域里，精致不是证据。

进入任何陌生地带时，先要名词和动词​——不是答案。你无法追问的答案，只是装饰。词汇才是那个让你从点头附和的人，变成能问出关键问题的人的东西。

有验证时，依靠验证。没有验证时，保持诚实。整条规则就是这样——而我注意到，它适用的地方远不止软件。

来源#

No Verification, No Claim

Image 1: A confident research verdict in elegant faded type — "the analysis is exhaustive and the conclusion inescapable… the matter may be considered settled" — struck through by a large red rubber stamp reading UNVERIFIED, NO CHECK WAS RUN 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.

What the prompt actually contains#

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.

The trap#

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.

No verification, no claim#

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.

The other half: expanding into the unknown#

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 habit, without the tool#

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.

Sources#