一句话定义：AI for Math 指把人工智能（尤其是大语言模型，LLM）真正用进数学研究——猜猜想、找反例、写证明草稿，再交给机器做严格的证明检查。
原理：一个爱吹牛的向导，配一个只认账的会计
数学研究像是在浓雾里找上山的路。LLM 读过海量论文，像一个嘴很溜的向导：它知道"这一带大概长什么样"，能快速说"往左拐试试""这个条件可能是多余的"。但它也会一本正经地记错路。所以关键不是信它，而是给它配一个不说谎的会计——证明助手（proof assistant，如 Lean、Isabelle）：你把推理写成它能读的脚本，它逐步检查，哪一步逻辑不合规就直接报错。
于是有三个典型动作：
1. 反例搜索。猜想往往死在反例上。模型负责"往哪找"（生成候选构造、缩小参数范围），数值搜索或进化式搜索负责"真去找"。
2. 证明生成。让模型写出自然语言证明草稿，把大问题拆成若干引理——这是它最擅长、也最容易出幻觉的地方。
3. 形式化验证。把草稿翻译成证明助手能检查的脚本，对错由内核按逻辑规则判定，"看起来对"没有用。
和邻居们的区别
| 概念 | 谁在判断对错 | 典型任务 |
|---|---|---|
| 符号/数值计算 | 确定性规则 | 求积分、解方程 |
| 自动定理证明（ATP） | 穷举式搜索 | 空间小但很深的推理 |
| AI 做数学题（benchmark） | 已有标准答案 | 竞赛题刷分 |
| AI for Math | 模型给启发式，验证器判对错 | 没有答案的开放猜想 |
最要紧的是最后一行：开放猜想没有标准答案可对，"对不对"只能靠证明本身的严格性。
"未发布成果"为什么吵得起来
数学界信任一个结果的方式只有一种：别人能独立复现检查。所以当有人宣称模型推翻了某个长期公开的猜想，却只给出结论摘要和对话截图，不公开完整证明、形式化脚本或可复现流程时，社区根本无从核对。讨论很快会从"数学突破"滑向"评审流程该怎样"。这不是保守，而是不可复现的宣称在数学里约等于零——无论说话的模型多强。
对你的实际意义
形式化验证器提供的是一种稀缺资源：可验证奖励。模型没法靠话术骗过检查器，所以它天然适合拿来做强化学习训练。反过来看，这套"生成者出方案、独立方判对错"的分工，是所有高风险场景用大模型的通用范式——别让写答案的人自己给自己判卷。
具体工具与模型的能力细节，以官方页面为准。