一句话定义：自动形式化（Autoformalization）指用 AI 把人类用自然语言和 LaTeX 写的数学命题、定义、证明，翻译成 Lean、Coq、Isabelle 这类证明助手（proof assistant）能逐行检查的形式代码。
它到底在做什么
这里有两步，很多人会混在一起：一是形式化"命题"，把"对任意 n≥3……"翻译成机器语言里的一句定理声明；二是形式化"证明"，写出让内核（kernel）接受的证明脚本。证明助手只做一件事：按规则逐条检查代码有没有漏洞。它不判断这个命题是否有趣，更不判断它是不是你想说的那句话。整条流水线里，唯一没有机器兜底的环节，恰恰是最关键的翻译环节。
打个比方：这像把一份中文合同翻译成一段机器可执行的合约代码。翻译时如果把"乙方应在 30 天内付款"写成"乙方可以付款"，代码照样编译通过、照样执行，只是它管的已经不是你的生意了。
可信度陷阱
最容易踩的坑是"证了个寂寞"：模型给出的形式化陈述比原命题弱——偷偷加上一个额外假设，或者把"无穷多个"写成"存在一个"——于是证明助手顺利通过，庆祝的却是另一件事。反过来，陈述写得太强，也会导致永远证不出来。
第二类坑是把"编译通过"当成"数学正确"。机器保证了推理链条无洞，但没保证定义、前提、常数取值与你脑子里那套语义一致。所以当"AI 推进了某个离散几何猜想"或"AI 攻克了某类流体方程难题"的消息出现时，社区的下一个动作通常是把它丢进 Lean 跑一遍，争论的落点也很少是"结论对不对"，而是"形式化出来的陈述还是不是原命题"。
和相邻概念的区别
| 概念 | 它在做什么 | 谁在兜底 |
|---|---|---|
| 自动形式化 | 自然语言 → 形式代码 | 只有人工核对陈述 |
| 自动定理证明 | 在形式系统里搜索证明 | 内核逐行检查 |
| 数值实验 | 算几个例子看像不像 | 没有兜底，只给直觉 |
| 通用大模型解题 | 直接写自然语言证明 | 没有兜底，靠人读 |
对从业者的意义
真正可落地的用法，不是"让 AI 直接证猜想"，而是：把关键引理形式化，当作审稿过滤器；把"我觉得这步显然"变成机器可查的一步；用形式化逼出那些被含糊表述盖住的额外假设。
实际使用时建议至少做三件事：人工逐字核对形式化后的陈述；把命题取反或故意削弱假设，看是否也能通过（能通过说明翻译有问题）；让没参与生成的人独立复现一遍。具体工具链与用法以官方文档为准。