大语言模型在数学研究中的应用：从证明草稿到定理证明辅助

先说明白这篇文章聊的不是“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看成“数学工作的协处理器”而不是“证明机”。它真正能帮上忙的地方是让那些大量重复、文献密集、结构繁琐的前期工作变得不那么消耗人。至于最终证明是否成立还是要靠形式化工具、同行评审和你自己的数学判断。如果你能把这两者结合起来现在就能把很多“不可能完成”的初期调研任务变成“只要花一个下午就能跑完的实验”。