这次我们来看一个不太一样的 AI 主题。不聊文生图、不聊视频生成也不聊 Agent 编排而是直接进入数学研究现场AI 到底能不能帮着解 Erdős 留下的那些经典谜题。先给结论以目前技术状态AI 还做不到“读完猜想自动给证明”但它的价值已经很明确——用暴力搜索帮你找反例用 SAT/SMT 求解器验证丢番图方程用 Lean 这类自动定理证明器把人类推理变成机器可检查的代码再用大语言模型批量生成候选递推规则交给执行器逐条筛错。整个流程本质上是猜想 - 建模 - 搜索 - 验证这也是人工智能走向纯数学研究前沿最务实的切入方式。这篇文章会从 Erdős–Straus 猜想入手带你跑通四条完整链路用 Python 做数论反例搜索用 Z3 求解器验证丢番图方程用 Lean 4 形式化一个数论命题用 LLM 批量生成并验证数学猜想。环境上不需要高价显卡CPU 就能跑大部分搜索任务。LLM 部分你可以用本地小模型也可以接云端 API。关键不是跑多大模型而是把“猜想建模”和“结果验证”这两件事做对。1. 核心能力速览AI 数学研究工具链能做到什么程度能力项说明目标问题Erdős–Straus 猜想、Collatz 循环检测、整数分解、形式化证明、数列规则猜测核心工具Python、SymPy、Z3、Lean 4、LLM 推理服务硬件门槛反例搜索类任务 CPU 即可本地大语言模型推理建议有独立显卡小模型 CPU 也能跑显存占用CPU 搜索几乎不占用显存本地 LLM 按模型参数量常见约 3GB 到 20GB 以上批量任务可在连续整数区间内批量扫描反例支持日志和断点续跑接口能力Z3 Python 接口、Lean 命令行接口、LLM HTTP API 都可脚本化调用启动方式手动安装工具链命令行启动无统一一键包核心限制AI 生成的结果必须经过验证器/证明器确认不能直接作为数学结论发布适合人群数学爱好者、算法工程师、AI 应用开发者、理论计算机方向学生这张表要传达的核心信息是这个方向不依赖单一模型而是一套工程组合拳。你不需要等“更强的 GPT”出现现在就能开始。我们下面要用到的工具分工非常清晰Python SymPy负责数值实验、分数运算、数列生成。Z3负责约束求解帮你判断某个方程在给定范围内是否有解。Lean 4负责形式化证明把数学命题写成机器可编译的代码。LLM 服务负责猜测规则、生成候选程序、解释反例模式。这套组合解决的问题不是“AI 取代数学家”而是“AI 把数学探索中重复、机械、容易出错的环节自动化”。2. 适用场景与使用边界AI 适合哪类数学问题不适合哪类先说适合的场景。**第一类反例搜索。**比如 Erdős–Straus 猜想我只需要验证“在某个 n 的范围内方程 4/n 1/x 1/y 1/z 是否都有正整数解”。人工计算慢但程序可以秒级扫完前几百个 n。这类任务非常适合机器批量处理。**第二类小规模 Diophantine 方程求解。**当变量有限、范围有限时Z3 这类 SMT 求解器非常可靠。你可以把方程写成约束让求解器搜索可行解。搜索不到解就是反例搜索到解就是验证。**第三类形式化证明。**Lean 4 这类工具把数学证明变成可编译的代码。你不需要相信某个 AI 的“推理过程”你只需要相信 Lean 的编译结果。AI 负责提出证明思路Lean 负责确认思路对不对。**第四类数列规律猜测。**给 LLM 一段数列让它猜递推公式再让 Python 验证前 100 项是否符合。这种“生成假设 程序验证”的方式比直接让 AI 给最终证明要可靠得多。再说边界。**AI 不能替代最终证明。**即使 LLM 看起来给出了很有说服力的推理最终结论也需要人类数学家或自动定理证明器确认。尤其是公开论文、课程作业、竞赛场合AI 输出不能直接当作人类推理依据。**不要用生成式模型处理未公开研究数据。**如果你在做一个尚未发表的新猜想把原始思路发给云端 API 会产生数据所有权和隐私问题。稳妥做法是本地部署小模型或者在脱敏之后再做推理。**版权与学术规范。**使用 AI 辅助数学研究时要遵守所在机构或期刊的声明要求。AI 发现的新公式、新证明序言能否写进论文、如何标注贡献需要按具体规则判断。**搜索不能证明“永远成立”。**程序扫描 n5 到 10^9不能证明 n10^91 也成立。搜索只能给直觉最终证明还是要靠数学方法。3. 技术路线选型探索一条数学猜想有四条路可走开始写代码之前先花两分钟把技术路线理清楚。不同路线解决不同层面的问题实际项目往往是组合使用。3.1 路线一暴力搜索与数值验证这是最容易上手的路线。把数学式翻译成代码指定 n 的范围程序逐项判断是否有解。这类任务适合 Collatz 循环检测、Erdős–Straus 分解验证、简单数论不等式的测试。优点是门槛低、结果直观。缺点是对于复杂问题搜索空间可能爆炸。比如暴力遍历三个变量极容易把 CPU 跑满几个小时。3.2 路线二SAT/SMT 求解器SAT/SMT 求解器处理“有限范围内是否存在解”这类问题非常高效。Z3 是微软开源的 SMT 求解器Python 绑定成熟。遇到丢番图方程、逻辑约束、组合优化问题时直接把它当“方程求解后端”来用。SMT 求解器的思路和暴力搜索不同暴力搜索是在枚举变量SMT 是在做约束传播和剪枝。因此它在处理带明显限制条件的问题时速度会快很多。3.3 路线三自动定理证明与形式化验证Lean 4、Coq、Isabelle 是主流的证明辅助工具。Lean 4 的社区生态最近几年增长很快Mathlib 数学库已经覆盖了本科和研究生阶段大量定理。路线三的核心价值是“可检查性”。你写下定理陈述再写证明脚本Lean 编译器会告诉你证明是否成立。相比 LLM 的“看似合理”Lean 给的是确定性结果。3.4 路线四LLM 生成猜测再交给验证器这条路线的实际形态是LLM 根据数列或问题描述生成候选公式、候选代码或候选证明策略然后你来执行代码或让形式化验证器确认。DeepMind 的 FunSearch 就是这个思路的代表LLM 生成代码片段评估器运行并保留得分高的片段再把高分片段反馈给 LLM 继续迭代。这种方式非常适合“搜索空间巨大但结果可验证”的问题。LLM 负责提出新候选项程序负责淘汰坏候选一轮一轮逼近更优结果。4. 本地环境准备从 Python 到 Lean 4下面开始搭环境。以下工具均可在 Windows、macOS、Linux 上安装关键是保持版本一致。4.1 Python 与数学库推荐 Python 3.10安装以下包pip install sympy z3-solver requestssympy负责分数运算和数论工具z3-solver是微软 Z3 的 Python 绑定位requests用于调用 LLM API。建议额外安装pandas用于记录批量搜索结果方便数据分析和导出pip install pandas matplotlib4.2 Lean 4 与工具链这里提供一个通用安装路径。具体命令以你本机操作系统为准Linux/macOS 推荐使用elan它是 Lean 4 的版本管理工具类似 Rust 生态的rustupWindows 上可以下载 Lean 4 官方 MSVC 构建或使用 WSL 安装 Linux 版本编辑器推荐 VS Code安装 Lean 4 扩展后即可自动识别.lean文件。安装完成后打开终端验证版本lean --version能看到Lean (version 4.x.x)就说明安装成功。注意首次创建 Lean 项目时Mathlib 依赖下载可能较慢建议保持网络稳定。4.3 LLM 服务LLM 部分有两种接入方式本地部署使用 Ollama、llama.cpp 或 vLLM 加载一个数学能力尚可的模型然后在127.0.0.1的本地端口调用。云端 API使用推理服务商提供的 HTTP API。下面所有示例都按照“替换 URL 和 model 名即可运行”的通用模板来写方便你接入自己的服务。5. 实操一用 Python 暴力搜索验证 Erdős–Straus 猜想Erdős–Straus 猜想的陈述非常短对任意整数 n ≥ 5方程4/n 1/x 1/y 1/z都存在正整数解 x、y、z。这个猜想几十年来一直未被证明但程序可以验证有限范围。先写一个简单版本直接枚举候选解并校验。from fractions import Fraction def find_erdos_straus(n, max_y10000): target Fraction(4, n) # 假设 x y z可以缩小 x 的搜索范围 # 由 1/x 4/n 得到 x n/4 # 由 4/n 1/x 1/y 1/z 3/x 得到 x 3n/4 x_start max(1, n // 4 1) x_end (3 * n) // 4 for x in range(x_start, x_end 1): for y in range(x, max_y 1): remaining target - Fraction(1, x) - Fraction(1, y) if remaining 0: continue # 如果 remaining 是一个单位分数 1/z就找到了一组解 if remaining.numerator 1: z remaining.denominator return x, y, z return None for n in range(5, 21): result find_erdos_straus(n) if result: x, y, z result check Fraction(1, x) Fraction(1, y) Fraction(1, z) print(fn{n:2d}: 4/{n} 1/{x} 1/{y} 1/{z} 校验: {check}) else: print(fn{n:2d}: 在搜索范围内未找到解)代码里做了一个关键优化假设x y z这样就能用两个数论不等式把 x 的范围卡在(n/4, 3n/4]之间。这比从 1 开始穷举快非常多。运行后前几个 n 的结果会类似n 5: 4/5 1/2 1/4 1/20 校验: 4/5 n 6: 4/6 1/2 1/12 1/12 校验: 2/3 n 7: 4/7 1/2 1/28 1/28 校验: 4/7 n 8: 4/8 1/4 1/6 1/12 校验: 1/2 n 9: 4/9 1/3 1/12 1/36 校验: 4/9 n10: 4/10 1/4 1/8 1/40 校验: 2/5判断成功的标准很简单每个 n 都有输出且check值等于左边的目标分数。如果某个 n 在搜索范围内没有输出就从三个方向排查max_y设小了有些解的 y 或 z 会很大x 的上下界裁剪出了问题检查整除和取整逻辑代码的分数运算被 Fraction 自动化简导致remaining.numerator 1判断失效。这里再强调一次程序跑通不代表猜想被证明只是说明在有限的 n 和变量范围里没有找到反例。真正的证明还需要数学推导。6. 实操二用 Z3 求解丢番图方程并检查反例直接把 Erdos–Straus 方程翻译成 Z3 约束让求解器去找整数解。这种方式比暴力搜索更适合变量间有复杂约束的场景。from z3 import Ints, Solver, sat def solve_erdos_straus(n, limit1000): x, y, z Ints(x y z) solver Solver() # 正整数约束 solver.add(x 0) solver.add(y 0) solver.add(z 0) # 假设 x y z交换顺序不影响解的存在性 solver.add(x y, y z) # 4/n 1/x 1/y 1/z # 两边同乘 n*x*y*z 得到 solver.add(4 * x * y * z n * (x * y x * z y * z)) # 为避免无限搜索限制变量上界 solver.add(x limit) solver.add(y limit) solver.add(z limit) if solver.check() sat: model solver.model() return ( model[x].as_long(), model[y].as_long(), model[z].as_long() ) return None for n in range(5, 31): result solve_erdos_straus(n) if result: print(fn{n:2d}: 解为 {result}) else: print(fn{n:2d}: 在 limit{1000} 范围内未找到解)这里的核心是把分式方程转换成整数方程4xyz n(xy xz yz)消去分母之后Z3 只需要在线性域内做整数约束求解。判断成功的标准每个 n 都能输出一个三元组且代入原公式后左右相等。如果某个 n 返回“未找到”常见原因有两个变量上界limit太低真实解超出了搜索范围方程约束有笔误两边乘分式的过程写错了。验证约束是否正确的简单办法取一个已知解代入约束表达式看能否通过。Z3 的优势在于你不需要手写搜索策略。它的底层会自动做约束传播、分支和冲突分析对很多丢番图方程来说效率比循环枚举高得多。7. 实操三用 Lean 4 形式化一个数论命题如果你希望 AI 的数学结论真正做到“机器可检查”Lean 4 是目前最值得投入的形式化验证工具之一。它不会接受含糊的推理所有证明都必须是确定性的代码。下面这段 Lean 4 代码来自一个非常基础的数论命题自然数加法满足交换律。这看起来简单但形式化验证的每一个步骤都会被编译器检查。import Mathlib -- 验证简单恒等式1 1 2 example : 1 1 2 : by rfl -- 自然数加法交换律 example (a b : ℕ) : a b b a : by omega第一段rfl是“定义上相等”的证明Lean 直接计算左右两边是否相等。第二段omega是一个决策过程能自动处理线性整数算术的证明。这是 Lean 社区常用的自动化工具之一。你在 VS Code 里打开这个.lean文件Lean 会实时显示检查结果。如果某一行的右侧出现蓝色或绿色图标说明证明通过如果出现红色错误说明证明有缺口。对于更复杂的数论命题比如“两个整数的最大公约数存在”写法会复杂很多需要导入 Mathlib 的数论模块import Mathlib.Data.Nat.GCD example (a b : ℕ) : ∃ g, Nat.gcd a b g : by exact ⟨Nat.gcd a b, rfl⟩这里我们直接构造出Nat.gcd a b作为存在的验证。证明虽然短但它展示了形式化数学的基本形态每条结论都要落到具体的定义和计算上。Lean 4 适合做什么适合把论文里的关键引理形式化适合验证数学算法的实现也适合把 AI 生成的“证明片段”变成机器可读的检查对象。需要注意Lean 4 的学习曲线比较陡。第一次写会频繁遇到语法错误建议从rfl、simp、omega这类自动化策略开始逐步过渡到更复杂的证明。8. 实操四用 LLM 辅助数学猜想与 API 批量调用LLM 在纯数学研究里不是用来做最终判断的而是用来做“假设生成器”。给它一段数列让它猜递推公式给它一个问题背景让它生成反例搜索代码给一个证明卡点让它给出多个解决思路再让验证器来判断。下面这个例子把“数列规则猜测”封装成一次 API 调用。假设你有本地 Ollama 服务模型名替换为你实际拉取的模型。import requests import json # 请替换为你的实际 LLM 服务地址和模型名 url http://127.0.0.1:11434/api/generate prompt 数列前几项如下 a(1) 1 a(2) 1 a(3) 2 a(4) 3 a(5) 5 a(6) 8 请给出 1. 一个可能的递推公式 2. 用 Python 验证前 20 项的代码 3. 该公式是否可能是唯一解给出理由。 payload { model: qwen2.5-math, # 替换为你本地或云端的模型 prompt: prompt, stream: False, temperature: 0.2, max_tokens: 1024, } resp requests.post(url, jsonpayload, timeout120) data resp.json() print(data.get(response, data))拿到 LLM 的回复后不要直接信任。把回复里的 Python 代码提取出来放到本地执行看看前 20 项是否真的匹配。如果匹配再继续扩大验证到前 100 项、前 1000 项。如果要批量处理多个数列可以做一层循环sequences [ 1, 1, 2, 3, 5, 8 AI数学研究实战：从反例搜索到形式化验证
这次我们来看一个不太一样的 AI 主题。不聊文生图、不聊视频生成也不聊 Agent 编排而是直接进入数学研究现场AI 到底能不能帮着解 Erdős 留下的那些经典谜题。先给结论以目前技术状态AI 还做不到“读完猜想自动给证明”但它的价值已经很明确——用暴力搜索帮你找反例用 SAT/SMT 求解器验证丢番图方程用 Lean 这类自动定理证明器把人类推理变成机器可检查的代码再用大语言模型批量生成候选递推规则交给执行器逐条筛错。整个流程本质上是猜想 - 建模 - 搜索 - 验证这也是人工智能走向纯数学研究前沿最务实的切入方式。这篇文章会从 Erdős–Straus 猜想入手带你跑通四条完整链路用 Python 做数论反例搜索用 Z3 求解器验证丢番图方程用 Lean 4 形式化一个数论命题用 LLM 批量生成并验证数学猜想。环境上不需要高价显卡CPU 就能跑大部分搜索任务。LLM 部分你可以用本地小模型也可以接云端 API。关键不是跑多大模型而是把“猜想建模”和“结果验证”这两件事做对。1. 核心能力速览AI 数学研究工具链能做到什么程度能力项说明目标问题Erdős–Straus 猜想、Collatz 循环检测、整数分解、形式化证明、数列规则猜测核心工具Python、SymPy、Z3、Lean 4、LLM 推理服务硬件门槛反例搜索类任务 CPU 即可本地大语言模型推理建议有独立显卡小模型 CPU 也能跑显存占用CPU 搜索几乎不占用显存本地 LLM 按模型参数量常见约 3GB 到 20GB 以上批量任务可在连续整数区间内批量扫描反例支持日志和断点续跑接口能力Z3 Python 接口、Lean 命令行接口、LLM HTTP API 都可脚本化调用启动方式手动安装工具链命令行启动无统一一键包核心限制AI 生成的结果必须经过验证器/证明器确认不能直接作为数学结论发布适合人群数学爱好者、算法工程师、AI 应用开发者、理论计算机方向学生这张表要传达的核心信息是这个方向不依赖单一模型而是一套工程组合拳。你不需要等“更强的 GPT”出现现在就能开始。我们下面要用到的工具分工非常清晰Python SymPy负责数值实验、分数运算、数列生成。Z3负责约束求解帮你判断某个方程在给定范围内是否有解。Lean 4负责形式化证明把数学命题写成机器可编译的代码。LLM 服务负责猜测规则、生成候选程序、解释反例模式。这套组合解决的问题不是“AI 取代数学家”而是“AI 把数学探索中重复、机械、容易出错的环节自动化”。2. 适用场景与使用边界AI 适合哪类数学问题不适合哪类先说适合的场景。**第一类反例搜索。**比如 Erdős–Straus 猜想我只需要验证“在某个 n 的范围内方程 4/n 1/x 1/y 1/z 是否都有正整数解”。人工计算慢但程序可以秒级扫完前几百个 n。这类任务非常适合机器批量处理。**第二类小规模 Diophantine 方程求解。**当变量有限、范围有限时Z3 这类 SMT 求解器非常可靠。你可以把方程写成约束让求解器搜索可行解。搜索不到解就是反例搜索到解就是验证。**第三类形式化证明。**Lean 4 这类工具把数学证明变成可编译的代码。你不需要相信某个 AI 的“推理过程”你只需要相信 Lean 的编译结果。AI 负责提出证明思路Lean 负责确认思路对不对。**第四类数列规律猜测。**给 LLM 一段数列让它猜递推公式再让 Python 验证前 100 项是否符合。这种“生成假设 程序验证”的方式比直接让 AI 给最终证明要可靠得多。再说边界。**AI 不能替代最终证明。**即使 LLM 看起来给出了很有说服力的推理最终结论也需要人类数学家或自动定理证明器确认。尤其是公开论文、课程作业、竞赛场合AI 输出不能直接当作人类推理依据。**不要用生成式模型处理未公开研究数据。**如果你在做一个尚未发表的新猜想把原始思路发给云端 API 会产生数据所有权和隐私问题。稳妥做法是本地部署小模型或者在脱敏之后再做推理。**版权与学术规范。**使用 AI 辅助数学研究时要遵守所在机构或期刊的声明要求。AI 发现的新公式、新证明序言能否写进论文、如何标注贡献需要按具体规则判断。**搜索不能证明“永远成立”。**程序扫描 n5 到 10^9不能证明 n10^91 也成立。搜索只能给直觉最终证明还是要靠数学方法。3. 技术路线选型探索一条数学猜想有四条路可走开始写代码之前先花两分钟把技术路线理清楚。不同路线解决不同层面的问题实际项目往往是组合使用。3.1 路线一暴力搜索与数值验证这是最容易上手的路线。把数学式翻译成代码指定 n 的范围程序逐项判断是否有解。这类任务适合 Collatz 循环检测、Erdős–Straus 分解验证、简单数论不等式的测试。优点是门槛低、结果直观。缺点是对于复杂问题搜索空间可能爆炸。比如暴力遍历三个变量极容易把 CPU 跑满几个小时。3.2 路线二SAT/SMT 求解器SAT/SMT 求解器处理“有限范围内是否存在解”这类问题非常高效。Z3 是微软开源的 SMT 求解器Python 绑定成熟。遇到丢番图方程、逻辑约束、组合优化问题时直接把它当“方程求解后端”来用。SMT 求解器的思路和暴力搜索不同暴力搜索是在枚举变量SMT 是在做约束传播和剪枝。因此它在处理带明显限制条件的问题时速度会快很多。3.3 路线三自动定理证明与形式化验证Lean 4、Coq、Isabelle 是主流的证明辅助工具。Lean 4 的社区生态最近几年增长很快Mathlib 数学库已经覆盖了本科和研究生阶段大量定理。路线三的核心价值是“可检查性”。你写下定理陈述再写证明脚本Lean 编译器会告诉你证明是否成立。相比 LLM 的“看似合理”Lean 给的是确定性结果。3.4 路线四LLM 生成猜测再交给验证器这条路线的实际形态是LLM 根据数列或问题描述生成候选公式、候选代码或候选证明策略然后你来执行代码或让形式化验证器确认。DeepMind 的 FunSearch 就是这个思路的代表LLM 生成代码片段评估器运行并保留得分高的片段再把高分片段反馈给 LLM 继续迭代。这种方式非常适合“搜索空间巨大但结果可验证”的问题。LLM 负责提出新候选项程序负责淘汰坏候选一轮一轮逼近更优结果。4. 本地环境准备从 Python 到 Lean 4下面开始搭环境。以下工具均可在 Windows、macOS、Linux 上安装关键是保持版本一致。4.1 Python 与数学库推荐 Python 3.10安装以下包pip install sympy z3-solver requestssympy负责分数运算和数论工具z3-solver是微软 Z3 的 Python 绑定位requests用于调用 LLM API。建议额外安装pandas用于记录批量搜索结果方便数据分析和导出pip install pandas matplotlib4.2 Lean 4 与工具链这里提供一个通用安装路径。具体命令以你本机操作系统为准Linux/macOS 推荐使用elan它是 Lean 4 的版本管理工具类似 Rust 生态的rustupWindows 上可以下载 Lean 4 官方 MSVC 构建或使用 WSL 安装 Linux 版本编辑器推荐 VS Code安装 Lean 4 扩展后即可自动识别.lean文件。安装完成后打开终端验证版本lean --version能看到Lean (version 4.x.x)就说明安装成功。注意首次创建 Lean 项目时Mathlib 依赖下载可能较慢建议保持网络稳定。4.3 LLM 服务LLM 部分有两种接入方式本地部署使用 Ollama、llama.cpp 或 vLLM 加载一个数学能力尚可的模型然后在127.0.0.1的本地端口调用。云端 API使用推理服务商提供的 HTTP API。下面所有示例都按照“替换 URL 和 model 名即可运行”的通用模板来写方便你接入自己的服务。5. 实操一用 Python 暴力搜索验证 Erdős–Straus 猜想Erdős–Straus 猜想的陈述非常短对任意整数 n ≥ 5方程4/n 1/x 1/y 1/z都存在正整数解 x、y、z。这个猜想几十年来一直未被证明但程序可以验证有限范围。先写一个简单版本直接枚举候选解并校验。from fractions import Fraction def find_erdos_straus(n, max_y10000): target Fraction(4, n) # 假设 x y z可以缩小 x 的搜索范围 # 由 1/x 4/n 得到 x n/4 # 由 4/n 1/x 1/y 1/z 3/x 得到 x 3n/4 x_start max(1, n // 4 1) x_end (3 * n) // 4 for x in range(x_start, x_end 1): for y in range(x, max_y 1): remaining target - Fraction(1, x) - Fraction(1, y) if remaining 0: continue # 如果 remaining 是一个单位分数 1/z就找到了一组解 if remaining.numerator 1: z remaining.denominator return x, y, z return None for n in range(5, 21): result find_erdos_straus(n) if result: x, y, z result check Fraction(1, x) Fraction(1, y) Fraction(1, z) print(fn{n:2d}: 4/{n} 1/{x} 1/{y} 1/{z} 校验: {check}) else: print(fn{n:2d}: 在搜索范围内未找到解)代码里做了一个关键优化假设x y z这样就能用两个数论不等式把 x 的范围卡在(n/4, 3n/4]之间。这比从 1 开始穷举快非常多。运行后前几个 n 的结果会类似n 5: 4/5 1/2 1/4 1/20 校验: 4/5 n 6: 4/6 1/2 1/12 1/12 校验: 2/3 n 7: 4/7 1/2 1/28 1/28 校验: 4/7 n 8: 4/8 1/4 1/6 1/12 校验: 1/2 n 9: 4/9 1/3 1/12 1/36 校验: 4/9 n10: 4/10 1/4 1/8 1/40 校验: 2/5判断成功的标准很简单每个 n 都有输出且check值等于左边的目标分数。如果某个 n 在搜索范围内没有输出就从三个方向排查max_y设小了有些解的 y 或 z 会很大x 的上下界裁剪出了问题检查整除和取整逻辑代码的分数运算被 Fraction 自动化简导致remaining.numerator 1判断失效。这里再强调一次程序跑通不代表猜想被证明只是说明在有限的 n 和变量范围里没有找到反例。真正的证明还需要数学推导。6. 实操二用 Z3 求解丢番图方程并检查反例直接把 Erdos–Straus 方程翻译成 Z3 约束让求解器去找整数解。这种方式比暴力搜索更适合变量间有复杂约束的场景。from z3 import Ints, Solver, sat def solve_erdos_straus(n, limit1000): x, y, z Ints(x y z) solver Solver() # 正整数约束 solver.add(x 0) solver.add(y 0) solver.add(z 0) # 假设 x y z交换顺序不影响解的存在性 solver.add(x y, y z) # 4/n 1/x 1/y 1/z # 两边同乘 n*x*y*z 得到 solver.add(4 * x * y * z n * (x * y x * z y * z)) # 为避免无限搜索限制变量上界 solver.add(x limit) solver.add(y limit) solver.add(z limit) if solver.check() sat: model solver.model() return ( model[x].as_long(), model[y].as_long(), model[z].as_long() ) return None for n in range(5, 31): result solve_erdos_straus(n) if result: print(fn{n:2d}: 解为 {result}) else: print(fn{n:2d}: 在 limit{1000} 范围内未找到解)这里的核心是把分式方程转换成整数方程4xyz n(xy xz yz)消去分母之后Z3 只需要在线性域内做整数约束求解。判断成功的标准每个 n 都能输出一个三元组且代入原公式后左右相等。如果某个 n 返回“未找到”常见原因有两个变量上界limit太低真实解超出了搜索范围方程约束有笔误两边乘分式的过程写错了。验证约束是否正确的简单办法取一个已知解代入约束表达式看能否通过。Z3 的优势在于你不需要手写搜索策略。它的底层会自动做约束传播、分支和冲突分析对很多丢番图方程来说效率比循环枚举高得多。7. 实操三用 Lean 4 形式化一个数论命题如果你希望 AI 的数学结论真正做到“机器可检查”Lean 4 是目前最值得投入的形式化验证工具之一。它不会接受含糊的推理所有证明都必须是确定性的代码。下面这段 Lean 4 代码来自一个非常基础的数论命题自然数加法满足交换律。这看起来简单但形式化验证的每一个步骤都会被编译器检查。import Mathlib -- 验证简单恒等式1 1 2 example : 1 1 2 : by rfl -- 自然数加法交换律 example (a b : ℕ) : a b b a : by omega第一段rfl是“定义上相等”的证明Lean 直接计算左右两边是否相等。第二段omega是一个决策过程能自动处理线性整数算术的证明。这是 Lean 社区常用的自动化工具之一。你在 VS Code 里打开这个.lean文件Lean 会实时显示检查结果。如果某一行的右侧出现蓝色或绿色图标说明证明通过如果出现红色错误说明证明有缺口。对于更复杂的数论命题比如“两个整数的最大公约数存在”写法会复杂很多需要导入 Mathlib 的数论模块import Mathlib.Data.Nat.GCD example (a b : ℕ) : ∃ g, Nat.gcd a b g : by exact ⟨Nat.gcd a b, rfl⟩这里我们直接构造出Nat.gcd a b作为存在的验证。证明虽然短但它展示了形式化数学的基本形态每条结论都要落到具体的定义和计算上。Lean 4 适合做什么适合把论文里的关键引理形式化适合验证数学算法的实现也适合把 AI 生成的“证明片段”变成机器可读的检查对象。需要注意Lean 4 的学习曲线比较陡。第一次写会频繁遇到语法错误建议从rfl、simp、omega这类自动化策略开始逐步过渡到更复杂的证明。8. 实操四用 LLM 辅助数学猜想与 API 批量调用LLM 在纯数学研究里不是用来做最终判断的而是用来做“假设生成器”。给它一段数列让它猜递推公式给它一个问题背景让它生成反例搜索代码给一个证明卡点让它给出多个解决思路再让验证器来判断。下面这个例子把“数列规则猜测”封装成一次 API 调用。假设你有本地 Ollama 服务模型名替换为你实际拉取的模型。import requests import json # 请替换为你的实际 LLM 服务地址和模型名 url http://127.0.0.1:11434/api/generate prompt 数列前几项如下 a(1) 1 a(2) 1 a(3) 2 a(4) 3 a(5) 5 a(6) 8 请给出 1. 一个可能的递推公式 2. 用 Python 验证前 20 项的代码 3. 该公式是否可能是唯一解给出理由。 payload { model: qwen2.5-math, # 替换为你本地或云端的模型 prompt: prompt, stream: False, temperature: 0.2, max_tokens: 1024, } resp requests.post(url, jsonpayload, timeout120) data resp.json() print(data.get(response, data))拿到 LLM 的回复后不要直接信任。把回复里的 Python 代码提取出来放到本地执行看看前 20 项是否真的匹配。如果匹配再继续扩大验证到前 100 项、前 1000 项。如果要批量处理多个数列可以做一层循环sequences [ 1, 1, 2, 3, 5, 8