先说明白：这篇文章聊的，不是“AI能不能替代数学家”，而是更具体的“AI，尤其是大语言模型（LLM），在重大数学发展里到底有哪些已经成熟、正在尝试，或者至少值得一试的应用示例”。所谓重大数学发展，可以粗略理解成：一个新猜想被提出，一个悬置多年的老猜想出现关键证明，或者某个大型研究计划进入了新阶段。这类工作通常有几个共同特征：文献量大、推理链长、符号体系复杂、需要反复验证。LLM进入这个场景的价值，不是直接给你一个已完成、可发表的证明，而是把原本需要几周甚至几个月才能做完的整理、枚举、转译和初步验证工作压缩到几天。
适合阅读这篇文章的，主要是三类人：一是做数学或数学物理研究的人，想了解AI工具现在能顶到哪一步；二是做形式化验证、定理证明辅助工具的工程师，想知道LLM怎么接入Lean、Isabelle这类流程；三是对AI for Math感兴趣的开发者。我的基本判断是：现在的LLM还远远没有到“自动解决重大数学难题”的阶段，但它足够做一套“先产生候选结果，再由人来验证”的科研协作流水线。下面我会按实际落地顺序，讲清楚能做什么、不能做什么、用什么判断标准以及踩了哪些坑。
1. 先想清楚：LLM在数学发展里做的是“参考系”而不是“答案机”
1.1 数学任务和通用文本任务的区别
很多人第一次用LLM做数学题，第一反应是“它能解微积分、能写证明，那是不是也能推动数学研究？”这种判断容易踩坑。普通问答里的数学题，大多有明确答案、固定解法、短逻辑链，模型只要见过类似例题，就能模仿出一篇看起来合理的解答。但重大数学发展里的问题，通常不是“计算一道题”，而是“在一堆已知结论和未验证假设之间搭建新的逻辑路径”。后者对逻辑自洽性、符号一致性、引用可靠性的要求极高，而这些恰恰是概率生成模型的天然弱点。
更准确地说，LLM给的是“有可能成立的参考系”，不是“已经证明的真理”。它可以帮你快速找到可能的思路、可能遗漏的引理、可能存在反例的方向，但它给出的每一步都需要重新验证。把模型输出直接当证明用，是这类工作流里最大的失败原因。
所以我的建议是：一开始就要给LLM设定正确的角色。它不是“证明机”，而是“科研助手里的第一阶段筛选器”。你在前面做问题拆解，它负责生成候选假设、整理文献线索、翻译证明草稿，最后由你或者形式化工具负责验证。这样既能发挥它的广度和速度，又不至于被它的“流畅表达”带偏。
1.2 先用一个经典小定理建立判断直觉
我一般会建议用几道经典小定理来测试当前模型到底适合哪类任务。比如“证明根号2是无理数”“证明素数有无穷多个”这类基础但完整的证明。别觉得这些题目太简单，它们的价值在于：证明结构完整、逻辑链清晰、错误容易发现，你能快速判断模型是在“真正推理”，还是在“回忆相似文本”。
实测时你很快会发现几种典型现象：
- 模型能写出欧几里得素数无限证明的大体框架，但在“为什么若p1...pn的乘积加1的质因子不在列表中”这一步，偶尔会出现含糊表述。
- 有些模型会把“反证法”和“构造法”混在一起，读起来像证明，但实际存在循环论证。
- 有些模型会引用一个“显然成立”的引理，但这个引理本身就是目标命题。
这些现象不是模型太笨，而是它的训练目标决定了它更擅长“生成概率上合理的词序列”，而不是“维护一个贯穿全文的逻辑状态”。所以当你拿到一段证明，第一件事不是看它写得顺不顺，而是把它拆成步骤，逐条对照定义和前提，看有没有跳步。
用经典小定理建立基线之后，再拿它测试你研究领域里的中等难度问题。这样能形成一张“模型能力地图”：哪些任务它能稳定输出半成品，哪些任务它基本在胡说。有了这张地图，后续在大问题上才不会被一次漂亮输出误导。
1.3 重大数学发展中，LLM真正能插入的环节
如果只是一句“LLM能做数学”，太泛了。放到重大数学发展这个具体场景里，我觉得有三个环节最值得关注：
- 文献线索整理：大型研究计划往往有几百篇相关论文，LLM可以快速提取某条思路的相似定义、证明技巧、后续发展，并生成一份带公式的笔记。
- 候选命题与反例搜索：从已知定理做类比扩展，生成“如果满足这些条件，会不会有类似结论”的候选命题，同时提出可能让结论失效的边界例子。
- 证明草稿补全：研究人员有整体思路，但中间缺少某个引理，LLM可以补一个版本，再由人判断或交给形式化工具检查。
这三个环节的共同点：模型只负责“产出可能性”，真正做最终裁决的是人、数值实验或定理证明器。我不知道未来LLM会不会直接证明黎曼猜想，但我知道至少在当下，把它当“会读很多论文、检索速度快、但容易一本正经胡说”的实习生来用，更合适。
2. 一个可复现的最小案例：让LLM帮忙整理证明思路
2.1 准备环境和输入构造
先不要一步到位部署大模型。做这类实验，入门阶段用API或者在线Demo就够了，重点是“怎么把数学问题写成模型能吃透的提示词”。我在实际测试时发现，很多人不是模型选错，而是问题描述太含糊。数学证明任务必须把三样东西写清楚：
- 目标命题：用标准数学符号写清楚要证明什么。
- 可用工具：允许使用哪些已证明的定理、定义、公理。
- 输出格式：要求模型给出定义、证明思路、关键步骤、待验证风险点，而不是一段“散文式证明”。
下面是我常用的一种提示词框架，你可以根据自己的任务调整：
【任务】 请帮我拆解下面这个命题的证明思路。 【目标命题】 对任意满足条件 H 的对象 X，证明性质 P(X) 成立。 【已知工具】 1. 已有定理 A，说明 ...； 2. 基本不等式或性质 B，说明 ...； 3. 可以使用反证法、归纳法、构造法等标准证明方法。 【输出要求】 1. 先列出题目中需要明确的所有符号、定义和假设。 2. 给出证明的主思路，不要一步一步写满，但要让读者知道整体走向。 3. 对每个关键步骤，标注“优先级：必须验证”。 4. 额外指出这个思路可能失败的地方，或者可能存在的反例。 【注意】 如果某个步骤引用了未说明的引理，请单独列出，并说明为什么需要它。这个模板的核心作用不是让模型直接输出“完美证明”，而是让它在可控范围内给出结构化的半成品。我在实际使用时会发现，一旦要求模型“标出必须验证的步骤”，它的生成质量会明显好很多，因为提示词迫使它把隐含假设暴露出来。
2.2 判断一个输出是否值得继续投入
模型输出了一段内容，接下来不是直接信，也不是直接丢。要快速做一轮“可投入度”判断，我的标准很简单：能不能把输出翻译成一系列可检查的步骤。如果输出只是一大段流畅的自然语言，没有任何定义、引理、条件分类，那基本不能用于研究场景。
下面这张表可以帮你快速区分可用输出和垃圾输出：
| 维度 | 可用输出 | 垃圾输出 |
|---|---|---|
| 符号定义 | 对每个变量、集合、映射都有说明 | 使用未定义的符号，或同一符号在不同位置含义不同 |
| 逻辑关系 | 步骤之间明显是从前提到结论的推进 | 前面讲A，后面突然跳到结论C，缺少B |
| 引理引用 | 明确说“引用定理X，条件是...”，并且条件确实满足 | 提到一个听起来很专业但不存在的定理名 |
| 风险标注 | 会指出哪一步需要验证、哪里可能有反例 | 每一步都像“显然成立” |
| 可验证性 | 能提取出具体条件，放到数值实验或证明器里试 | 都是空泛的逻辑连接词，没有可执行内容 |
在收到第一次输出后，我会先把“待验证风险点”提取出来，作为下一步验证清单。比如模型说“这里需要使用柯西-施瓦茨不等式，但需要先确认函数在区间上平方可积”，那我接下来就去检查这个平方可积条件是否满足。如果不满足，这条路线可能要先修正，而不是继续往下走。
2.3 从单条测试到批量评估
一旦单条任务跑通了，你会想同时测试多个问题、多个模型，或者多个提示词版本。这里一定要控制节奏。我一开始踩过一个坑：写了一个循环，一口气提交了50个证明任务，结果很快触发了接口限流，而且有一大半输出因为输入格式错误被截断，最后只能重新跑。
更稳妥的方式是分三步：
- 批次规模先压到5到10条。跑通之后检查每条输出是否进入预期目录、是否占用太多资源、是否有异常报错。
- 给每条任务设置唯一ID，把模型名称、提示词版本、输入命题、输出结果、人工评级都记录到一张表里。这样才能回溯是哪一轮改动导致质量下降。
- 开一个小型队列，不要一次性并发太多。如果使用API，可以限制每秒或每分钟的请求数；如果本地部署，则需要观察显存和GPU利用率，避免多个任务相互争抢。
这样做的好处是，后续你可以对每次实验做清晰的对比。毕竟在数学研究里，很多东西没法用“感觉更好”来评判，把结果结构化之后，才能用数据说话。
3. 在重大数学发展里，更常见的三类落地点
3.1 猜想形成阶段：让模型生成候选命题和特例
重大数学发展很少是凭空冒出来的，很多时候是先有大量数值实验和类比，再被凝练成猜想。LLM在这个阶段能做两件事：一是生成“类比命题”，二是生成“可能让命题失败的特例”。
举个例子，你已知某个定理在“有限生成群”条件下成立，那你自然想问：在“可数生成群”或者“有限表示群”条件下，结论还能不能成立？这种问题对数学家来说需要翻阅很多文献，因为“是否有人研究过”本身就是信息。LLM可以帮你在大量论文摘要、综述、知识库中做初步匹配，并生成“从已知结果看，条件变化后最可能失效的是哪一步”的判断。
同时，它会根据已有定理的证明结构，列出可能破坏结论的边界例子。比如“如果换成分裂域”“如果去掉紧致性条件”“如果不要求光滑只是连续”等等。这些候补特例不一定对，但它们能帮助你快速缩小搜索空间。我自己的习惯是：把模型生成的特例拿到数值计算软件里快速验证，能筛掉一大批明显错误，剩下那些不容易验证的，再人工攻。
当然，这条路的局限也很明显：模型没有真正的“数学直觉”，它靠的是训练语料里的统计关联。所以它能给出的类比通常很直接，不太可能产生那种需要跨领域抽象才能发现的深刻猜想。把它当成“灵感收集器”比当成“新时代拉马努金”更实际。
3.2 交互式定理证明：用LLM辅助Lean等证明脚本
这是目前我觉得最接近“工程可落地”的方向之一。Lean、Isabelle、Coq这些交互式定理证明器，要求每一个证明步骤都能被机器检查。以往写这类形式化证明非常耗时，尤其是从自然语言草稿翻译成形式化策略。LLM擅长的是“看到当前证明状态，生成下一步要执行的策略”，这个模式非常适合接入证明器。
流程大致是：
- 在Lean里把定理陈述写成标准形式，例如一个目标命题。
- 把当前“证明状态”（goal）和已有的上下文喂给LLM。
- 让模型生成一系列策略或中间断言。
- 把模型输出交给Lean执行，查看是否通过。
这里有个关键认知：模型不需要一次写完整份证明，它只需要生成“下一步”或者“下一步的一小段”，然后通过证明器反馈来修正。这种交互模式利用了证明器的确定性，弥补了模型的概率性。换句话说，模型负责“出招”，证明器负责“验证”，二者配合得好的时候，会比我凭空让模型写完整证明稳定很多。
但也要注意坑：形式化证明的语法、库函数命名、策略选择都和具体版本强相关。同一个模型，在Lean4和Lean3上的表现可能差异巨大。所以不要直接拿网上老的示例代码跑，先确认你的Lean版本、Mathlib版本和运行环境都正确。报错信息里的“unknown identifier”经常不是模型思路错，而是库里的函数名变了。
3.3 长篇数学论述的梳理和交叉检查
一份重大证明草稿可能长达几百页，里面会反复引用前面已经证明过的引理、定义和记号。人工做全文一致性检查，既辛苦又容易漏。LLM虽然不能替你证明，但在“文本层面的结构梳理”上可以帮上大忙。
比如你可以把文档按章节切块喂给模型，让它输出每章使用了哪些定义、引理、定理和假设。然后把这些输出汇总成一张依赖表，交叉检查某个引理到底有没有被证明、有没有循环引用。这种做法本质上是在做“文档工程”，但它能把人的注意力集中在真正需要数学判断的地方，而不是耗在翻页和检索上。
再比如，你可以让模型检查“同一个符号在不同章节是否保持一致”，或者“某个定理的假设条件在使用时是否被再次验证”。这类任务不一定要求模型理解全部数学内容，它只需要对文本做结构化扫描，因此成功率较高。我用下来后最明显的感受是：这类辅助工作占用时间从原来的整个半天，缩短到半小时，而且因为输出结构统一，我还能继续用脚本做二次检查。
4. 判断模型能力的关键指标，以及怎么设置“及格线”
4.1 适合用LLM处理的数学任务特征
不是所有数学问题都适合交给LLM。结合我自己的测试，适合的任务通常有这几个特征：
- 允许启发式输出：目标是寻找思路、生成候选命题、整理文献，而不是一步到位证明。
- 有清晰验证手段：输出可以被数值实验、已有文献或形式化验证器检查，哪怕检查本身也要花时间。
- 逻辑链不超过一定长度：如果问题本身需要连续推理20步以上，当前模型很容易在中间某个位置出现断裂。
- 上下文相对完整：模型能看到足够多的定义、条件和样例，不需要“猜测”你脑中的隐含信息。
下面这张表是我给任务分类的参考：
| 任务类型 | 是否适合LLM | 说明 |
|---|---|---|
| 生成若干候选引理 | 适合 | 输出后需人工或计算验证 |
| 搜索反例的思路 | 比较适合 | 可以提供数值尝试方向，但需运行实验 |
| 自然语言证明翻译为形式化策略 | 中等 | 配合证明器反馈，可以逐步修正 |
| 数百页手稿的一致性检查 | 适合 | 属于文本结构任务，不是数学推理任务 |
| 直接证明未解大猜想 | 不适合 | 输出无法成为可验证的“证明”，除非后续流程极严格 |
要特别注意：即使任务“适合”，也只是一开始适合。真正落地时，模型的回答质量和你的提示词、验证机制、容错设计强相关。
4.2 哪些任务容易被模型的“流畅表达”骗过去
最容易翻车的数学任务，通常是那些“模型见过很多类似文本”的任务。比如常见的数论定理、经典不等式、基础群论结论，模型很容易在开头引用正确，中间开始堆砌已知结论，最后用一句“因此”收尾。表面上很完整，实际上并没有构造出有效的证明链。
更隐蔽的是“存在性证明”和“构造性证明”混合的任务。模型可能会说“定义映射f为该集合到另一集合的映射”，但完全没说明映射的存在性、良定义性，或者是否依赖于选择公理。对受过训练的人来说，这种跳步可以被发现；但如果只是读一遍，很容易被它的“专业感”迷惑。
因此，在大型数学发展里用LLM时，我建议对所有模型输出设置一个共同原则：任何没有被独立验证的声明，都只当作候选材料处理。哪怕它引用了某个定理，也要去查原文献，确认定理条件确实适用于当前情境。这不是不信任模型，而是概率模型本身的边界决定了它无法保证逻辑确定性。
4.3 怎么给模型输出设置“及格线”
“及格线”不是“模型回答得对不对”，而是“这份回答能不能进入下一步验证流程”。我一般用四个层次：
- L0：无法使用。输出混乱、符号未定义、逻辑跳跃，直接丢弃。
- L1：可以摘取片段。整体不可靠，但里面某几个例子、某个引理名称、某个数值方向有价值，可以提取出来。
- L2：可以进入半自动验证。输出结构完整，可分离出关键断言，我可以用计算脚本或证明器逐一检验。
- L3：可以作为草稿继续推进。大部分步骤都合理，需要补充的只是具体计算和细节整理。
用这个分级标准，每次模型输出后都有明确的去向，而不是笼统地“觉得还行”。在研究了几个真实案例之后，你会发现L2和L3的比例通常不高，但这并不代表LLM没用，因为L1里经常藏着有价值的线索。真正重要的，是你不能把L1当成L3来用。
5. 资源环境与批量化：本地、API和集群怎么选
5.1 入门阶段的最低配置
如果你只是想试一下这个主题，先不需要急着部署本地大模型。用常见API、开源模型的在线Demo，或者跑一个量化过的中小型模型，都可以完成大部分实验。这个阶段需要的不是满血的推理能力，而是低成本、快速迭代。
本地部署的低配参考大概是：16GB内存加一张8GB显存的GPU，能跑7B参数级别的量化模型，处理单条数学证明思路没问题，但速度不快。如果是13B、14B模型，最好有16GB以上显存；如果没有独显，只靠CPU也能跑，但你要有等待的心理准备，一个长文本生成任务可能要几分钟甚至更久。
比较稳妥的顺序是：先用API或在线环境验证提示词和流程，等确认这套流程有稳定价值后，再考虑本地部署。千万不要一开始就花大量时间配置服务，结果发现你的问题根本不适合LLM处理。
5.2 批量任务的资源管理和日志结构
当你开始批量测试，最重要的事情就不是单个模型有多强，而是任务管理有多规范。我建议至少记录以下信息：
| 字段 | 说明 |
|---|---|
| 任务ID | 每个输入的唯一编号，方便回溯 |
| 模型名称 | 包括版本号，例如“某个开源模型的7B量化版” |
| 提示词版本 | 因为你一定会多次修改提示词 |
| 输入命题 | 原始目标命题 |
| 输出文本 | 模型生成的完整结果 |
| 人工评级 | L0/L1/L2/L3 |
| 验证结果 | 是否通过了数值验证、证明器或人工检查 |
| 错误信息 | 如果有超时、截断、格式错误，记录原始异常 |
批量任务不要一上来就开最大并发。如果你的接口有限速，并发太大会直接触发429或者被断开；如果你本地部署，多个请求同时跑会导致显存溢出或响应时间急剧上升。我一般会从“1个并发”开始，跑通后再逐步增加到2、4、8，同时观察成功率和延迟的变化。
5.3 本地部署时我自己踩过的几个坑
本地部署数学任务时，最常遇到的问题不是模型不会推理，而是环境配置把你的时间吃掉了。列几个高频坑：
- 端口被占用：启动服务时提示“端口已被使用”，先查进程，不要直接换端口，因为你后面对接的代码可能写死了地址。
- 上下文长度限制：数学证明往往需要把前面的定义和引理塞进上下文，很多模型默认的context window不够用。生成到一半突然丢失前文，输出后半段就会跑偏。
- max_tokens限制：一次生成的最大长度设置太小，模型还没写完整就被截断。这个问题会把一个有潜力的证明思路切成残稿。
- 显存溢出：批量任务或长文本生成时最容易出现。解决办法一般是降低批量数、降低推理精度、或者切断超长输入。
我建议的排查顺序是：先用最短的输入做一次生成，确认服务能启动、输出不是空；然后逐步增加输入长度，观察显存和内存占用；最后再跑批量。这样你才能确定一个“最大安全输入长度”，避免后续任务集体失败。
6. 失败模式和排查顺序：为什么“模型说得对”不等于“证明是对的”
6.1 最常见的三类失败
用LLM做数学研究，失败是常态，关键是要识别它们。我遇到最多的三类失败是这样的：
- 幻觉引理：模型引用一个听起来很标准的定理，但实际并不存在，或者条件与当前命题不匹配。比如明明是在实变函数问题的证明里，突然搬出一个“据复分析里的某某定理”之类的说法。
- 符号漂移：同一个变量在文章前半段表示集合，后半段变成映射；或者“n”在第一个引理表示正整数，在第二个引理里变成某个生成元的个数。这种错误在长篇生成里几乎无法避免。
- 逻辑跳步：模型知道开头和结论，但中间省略了关键的构造或验证步骤。省略的原因可能是上下文被截断，也可能就是模型觉得“太简单不用写”。
这三种失败都不是偶发问题，而是概率生成模型的结构性特征。我们需要接受这个现实，然后用流程去兜底。
6.2 数学场景下的排查链路
如果模型输出出了问题，先不要急着换模型、调温度、改并发。我建议按下面的顺序排查：
- 先看输入提示词是否完整。目标命题、可用工具、输出格式是否写清楚？如果连“需要定义的符号”都没让模型写，它当然容易乱造。
- 再看模型输出中的变量、定理引用和逻辑步骤。把每一步单独拆出来，和原始定义、已知条件对照。重点不是“这句话通不通”，而是“这个变量的类型对不对”“这个引理的适用条件满不满足”。
- 如果输出是形式化证明脚本，运行证明器看具体报错。比如Lean的“unsolved goals”“type mismatch”会准确告诉你问题在哪一步。此时不要因为模型写了10行策略就忽略最后一行错误。
- 最后才调整模型或参数。温度、top_p这些参数主要影响随机性，不能解决逻辑断裂。如果同样的输入反复失败，问题多半不在参数，而在任务分解或验证机制。
我把这个顺序写成了一个清单，每次实验前都过一遍。你会发现，很多时候“模型不行”其实是输入材料或验证过程没跟上。
6.3 降低风险的具体策略
与其期待模型变得更强，不如在流程设计上降低风险。我常用的几招：
- 强制分步输出：在提示词里要求“先列出需要的引理，再给出证明思路”。这样即便最终证明失败，你也能拿到一份引理清单继续排查。
- 要求标注待验证声明：让模型对每个关键步骤标出“这里需要独立验证”。这可以逼它把隐含假设暴露出来。
- 自动抽查关键信息：把输出中的定理名、公式、变量提取出来，和已有论文或符号库做匹配。虽然不能验证逻辑，但能很快发现“引用一个不存在的定理”这种问题。
- 重要结论必须过证明器或人工复核：只要一条路线可能进入正式论文，就不能停留在“模型说可以”。
这些策略不会让模型变聪明，但它们能把“模型产生的噪音”控制在可管理的范围内。
7. 我的经验：先把“小定理跑通”再谈“重大发展”
7.1 从经典问题开始建立基线
如果你想在这个方向认真投入，我特别建议先花一两周时间做“小定理跑通”训练。选一个你熟悉的数学分支，找三到五个经典引理，让LLM给你生成证明思路，再逐条验证。不要选太容易的，也不要选世界难题，选那种“你完全知道标准证明，但过程有几步需要仔细检查”的问题。
记录下三个指标：
- 结构完整率：输出中是否有完整的定义、条件和结论。
- 可验证步骤比例：输出的步骤有多少能直接进入计算或证明器验证。
- 有效修正次数：在人工介入后，你需要修正多少次才能得到可靠证明。
这些数据会告诉你这个模型在你这个领域里到底处于什么水平。我测试下来，不同模型在不同数学分支上的表现差异很大，不能简单说“某模型擅长数学”。
7.2 把LLM当作科研流水线上的“第一阶段筛子”
在真正涉及重大数学发展的工作中，我更愿意把LLM看成“第一阶段筛子”。它的作用不是做最终判断，而是快速扩大搜索范围。比如一个研究方向有100种可能的路径，人的精力只能认真看5种，LLM可以帮你从100种里挑出15种“至少在文本层面没有明显矛盾”的路径，然后你再重点投入。
这个筛选过程不是“用模型代替判断”，而是“用模型降低试错成本”。一条路径会被淘汰，往往不是因为它在数学上真的不可行，而是因为资料查找和初步尝试的成本太高。LLM把这一步成本压下来之后，整个科研流程的推进速度会明显更快。
当然，这也意味着你需要有一套严格的“淘汰标准”。我习惯在筛选时就明确写出：什么样的情况算“值得继续”，什么样的情况算“直接放弃”。比如说，如果模型给出的证明思路在第一步就需要一个未被证明且看起来很难证的引理，那我可能立刻降低优先级；如果模型给出的主要困难恰好是当前研究计划里已经准备处理的步骤，那就可以继续。
7.3 给想入坑的人三条建议
最后给想在这个方向投入的人三条建议，都是我自己踩过坑以后才总结出来的：
- 从可验证的小问题入手，不要直接挑战大猜想。大猜想如果失败，你分不清是模型能力问题、提示词问题，还是这个猜想本身太难；小问题可以帮你把变量控制住。
- 给模型的输出预设验证机制，不留“可能对”的模糊地带。每一步输出都应该能映射到某个可执行检查：数值计算、已有文献、证明器、人工重写。
- 把每一次实验记录成可复现材料。包括提示词、模型版本、输入命题、输出结果、验证结论。没有记录，就无法判断自己是在进步，还是在原地打转。
我更倾向于把LLM看成“数学工作的协处理器”，而不是“证明机”。它真正能帮上忙的地方，是让那些大量重复、文献密集、结构繁琐的前期工作变得不那么消耗人。至于最终证明是否成立，还是要靠形式化工具、同行评审，和你自己的数学判断。如果你能把这两者结合起来，现在就能把很多“不可能完成”的初期调研任务变成“只要花一个下午就能跑完的实验”。
