LLM大语言模型在数学未来中的哲学前景by 芬纳・斯坦利・坦斯韦尔（Fenner Stanley Tanswell）、阿斯盖尔・贝格（Ásgeir Berg）

★置顶zzllrr小乐公众号，追踪《小乐数学科普》系列报道，参与数学 vs AI投票！

AI时代思考数学的未来。柏林工业大学和 冰岛大学的 两位学者分享大语言模型（LLM）在数学未来中的哲学前景。

本文关键词：

数学实践、大语言模型、证明、遵循规则悖论、反向半人马（ centaur，半人马，代指人和AI的结合体 ）、数学证成 （Justification，取自哲学概念术语，意为辩护、合理化） 、证明辅助器。

AI vs Math 投票火热进行中

（点击 zzllrr小乐 公众号任一近期文章参与投票）

Your Vote Matters! We Value Your Value!

作者：芬纳・斯坦利・坦斯韦尔（Fenner Stanley Tanswell，柏林工业大学）

阿斯盖尔・贝格（Ásgeir Berg，冰岛大学）

M×Φ 数学与哲学年鉴 Annals of Mathematics and Philosophy 2025-12-31

译者：zzllrr小乐（数学科普公众号）2026-7-1

求喜欢

摘要

本文考察大语言模型在不久的将来可能对数学实践产生的哲学影响。部分知名研究者提出，大语言模型很快将具备生成、核验证明的能力，为人类数学家卸下沉重负担。

但本文主张，大语言模型技术在数学领域的落地绝非仅作为中立工具、让数学家按原有方式开展工作，而是会给数学实践带来根本性变革，并伴随深刻的哲学意蕴。

本文论证，即便大语言模型的可靠度提升至远超当下的水平，我们也无法确信其输出会持续符合预期；并且由大语言模型生成的证明所提供的证成（Justification），永远无法成为严格意义上的数学证成。

本文评估计算机核验、人工复核两类解决路径，并论证二者均无法弥合这一哲学层面的鸿沟，无法产出真正的数学证成。

我设想未来，我们不再手动录入证明，而是向某款 GPT 口述思路，GPT 会同步将内容形式化到Lean证明系统中。一旦全部核验通过，GPT 大致会给出这样的反馈：“这是你的 LaTeX 论文，附带 Lean 形式化证明。如果你需要，我可以一键提交至期刊。”它会成为一款绝佳辅助工具。 —— 陶哲轩（Terence Tao）2024年6月

1）引自克里斯托夫・德罗塞尔（Christoph Drösser）2024年《科学美国人》访谈。

§1 引言

ChatGPT 等大语言模型问世后，迅速在社会、文化、技术层面掀起广泛影响。本文将探究这类技术在近期内对数学产生的哲学效应。大语言模型能够流畅读写自然语言与计算机代码，由此催生一种诱人设想：计算机系统或许能像数学家一样阅读、撰写、理解证明，这可能为数学带来颠覆性变革。

2）马丁（Martin）与皮斯（Pease）如此表述：“对人类互动与推理机制的深入理解，将为AI、计算数学与纯数学的交叉融合开辟全新路径…… 仍有大量研究有待开展，相关领域积累的研究体量庞大，最终成果或将彻底改变数学的研究与产出模式。”（马丁、皮斯，2013，第 115 页）

但这类技术同样充满争议。一部分人认为AI数学家的愿景已近在咫尺，另一部分人则指出，AI 看似具备理解能力，实则只是虚假幻象，底层并不具备智能推理能力。下文将梳理大语言模型在数学领域的哲学前景，在热潮与批判之间寻找中立公允的分析视角，客观评估其实际价值。

正如本文开篇引文陶哲轩所言，顶尖数学家已经预判，大语言模型技术将深度重塑数学实践，具体落地方式分为多种：最简单的是由大语言模型直接生成证明；

第二种用途是搭建桥梁，打通数学家日常使用的非形式语言与可由计算机核验的形式推导语言。这种将数学家自然书写的证明自动转化为形式证明的过程，被称作自动形式化（autoformalisation）；核心构想是人类撰写非形式证明，交由大语言模型完成形式转换，再由计算机完成核验。

第三种用途是作为AI助手，例如生成猜想示例与反例、从海量文献中检索相关定理、填充证明中的常规推导细节、为交互式证明辅助器提供形式化指引。本文不会重点讨论这类交互式应用，相关内容留待后续研究。

本文核心论点是：将大语言模型投入数学实践，绝非仅作为辅助工具维持原有研究模式，而是会带来根本性变革，伴随深刻哲学问题。这场变革是否值得接纳取决于多重因素，本文聚焦核心问题：我们能否信任数学专用大语言模型的输出符合预期。依托底层技术原理，本文论证：即便大语言可靠度无限提升，我们也无法保证其输出始终符合预期；大语言模型生成证明带来的证成，永远无法成为严格数学证成。本文分别评估计算机核验、人工复核两种补救方案，并证明二者均无法填补这一哲学缺口，无法生成真正的数学证成。

3）本文议题范围有限，暂不讨论大语言模型交互式使用、伦理问题。例如气候危机背景下大语言模型能耗极高（许策Schütze，2024）、AI 价值导向由科技企业而非数学家主导，给数学带来多重潜在风险（哈里斯Harris，2024）。

章节安排：

第2节，梳理计算机介入数学领域的哲学背景；

第3节，概述大语言模型工作原理，并评估其当下数学能力；

第4节，梳理针对大语言模型生成证明可靠性的基础质疑；

第5节，提出一套近似克里普克 - 维特根斯坦遵循规则悖论的认识论论证，指出大语言模型无法稳定与人类数学家共用同一套数学概念，进而丧失严格数学证成；

第6节，回应 “可人工复核 AI 证明” 这一观点，提出反向半人马论证：核验大语言模型证明的难度远高于人类证明，因此复核无法凭空产生数学证成；

第7节，评估自动形式化能否规避证明错误；

第8节，整合全文结论。

§2 证明、证成与计算机

大语言模型作为数学工具登场，是数学与计算交织发展史的全新篇章。这段历史的起点界定取决于定义：可以追溯到算盘、帕斯卡计算器、莱布尼茨步进计算器、巴贝奇差分机与分析机、洛夫莱斯最早的计算机程序、图灵机，或是现代计算机的诞生。

现代标志性事件是阿佩尔（Appel）与哈肯（Haken）1977年借助计算机完成四色定理证明。

4）需说明这并非首份计算机辅助证明，德特勒夫森（Detlefsen）与卢克（Luker）1980 年列举了更早案例。

这份证明包含海量分情况枚举，全部由计算机完成而非人工推导，由此引出哲学难题：仅由计算机核验的证明，是否能提供与传统证明同等规格的数学证成？蒂姆茨科（Tymoczko）甚至提出，这份证明根本算不上真正的证明：

“凭什么说四色定理并非真正定理、数学家没有给出完整证明？理由只有一条：没有任何数学家完整读过这份证明，也没有人见过‘该定理存在证明’的完整推演。且几乎不可能有数学家完整读完这份证明。”（蒂姆茨科，1979，第 58 页）

蒂姆茨科提出，这份所谓证明存在一处巨大缺口，只能依靠计算机实验填补。因此我们对该定理的认知只能是后天的，本质依赖计算机提供的经验实证。在蒂姆茨科看来，这与传统先天数学证成标准并不等同。此外计算机还存在编程、硬件故障两类出错风险，这绝非空想：任何大规模代码都难以规避程序错误，硬件故障同样会引发计算偏差，早期奔腾处理器著名的浮点除法缺陷便是典型，数学家托马斯・R・尼利（Thomas R. Nicely）在编写素数生成代码时发现了该漏洞。

我们还可以补充一个日常案例：即便硬件、程序完全按设计运行，计算机计算依然会出错。本文撰稿时，谷歌计算器计算 999999999999999 − 999999999999998，输出结果为 0，根源是浮点数处理大数的机制缺陷。核心结论是：只要计算机存在出错可能性，它就无法作为严格数学证成的来源。

5）单纯存在出错可能性不足以否定数学证成，否则将陷入普遍认知怀疑论。真正关键是何种出错风险具备可接受性。德托福利（De Toffoli）2021 年提出可错主义数学证成理论，“校准于人类社会共性与认知架构，包含人类固有局限”（德托福利，2021，第 824 页），但她并未定论计算机证明能否先天核验。

学界针对这类担忧存在诸多反驳观点。德特勒夫森（Detlefsen）、卢克（Luker，1980）提出，大量传统证明同样依赖人工计算不出错这一经验前提，二者并无优劣之分。也有观点认为，人类处理常规计算比计算机更容易出错，因此四色定理计算机证明的出错概率，反而低于冗长传统证明。从社会学事实来看，数学界已经普遍接纳四色定理证明，同类大规模计算机证明亦获得认可，例如标准数独最少 17 线索唯一解证明（麦圭尔（McGuire）等人，2014；帕希娜（Parshina），2024）。这份证明遍历全部 16 线索布局，均无唯一解，同时存在 17 线索合法谜题；如今几乎无人认为这份证明存在漏洞。

另一种回应是 “自主调整怀疑程度”（巴扎德（Buzzard），2024，第 219 页）：若担忧计算出错，可更换设备重复运算；仍存疑虑则将数学内容完整形式化，例如贡捷（Gonthier）2008 年对四色定理完成全形式核验。针对每一层疑虑，都存在对应的补救手段。

但核心分歧不在于宽泛意义上的证成，而在于专属的数学证成，学界普遍认为后者标准更高。即便一条数学论断拥有充足佐证（资深数学家证言等经验证据），也不代表获得了严格数学证成。核心问题是：证言、经验实证这类证成，与数学证成的本质区分是什么？

蒂姆茨科梳理了多条区分标准，其中与本文关联最紧密的是可综观性：

（可综观性，Surveyability，即可全览性）一份证明具备可综观性，当且仅当理性主体能够完整读懂、复盘、把握、核验证明整体。

6）维特根斯坦（Wittgenstein，2001，143-147）已讨论可综观性；阿祖尼（Azzouni，1994，166-171）、巴斯勒（Bassler，2006）、科尔曼（Coleman，2009）、塞科（Secco）与佩雷拉（Pereira，2017）、哈布古德 - 库特与坦斯韦尔，帕希娜（2024）均有相关论述；达斯顿（Daston，2019）梳理该概念完整思想史。

蒂姆茨科的论证是：大规模计算机证明超出人类个体的综观能力，因此不属于真正证明。可综观性的核心价值在于关联数学理解：一份可综观证明能让我们读懂全新数学内容，而计算机分情况枚举证明无法实现这一点。例如数独最少 17 线索证明，读完也无法让人理解为何临界数字是 17。

但研究解释性证明的文献指出，许多传统证明同样无法带来深层理解，因此可综观性不能作为区分数学证成与普通证成的唯一标准。

此外大量传统证明同样不具备可综观性，例如有限单群分类定理整合海量文献，总页数达数千页，没有任何数学家能完整通读、统一把握。若严格遵循可综观标准，这份学界广泛接纳的集体证明将被排除在外。尽管分类定理已获得普遍认可，但仍有充分理由保持审慎：参与项目的数学家坦言，证明篇幅过大必然伴随疏漏（斯泰因加特（Steingart），2012；哈布古德 - 库特（Habgood-Coote）、坦斯韦尔，2023），严格而言包含错误的证明不能算作证明。数学家给出务实定义 “可修正性”：

（可修正性 Fixability）一份证明具备可修正性，当相关领域专家无需开展全新重大数学工作，就能轻松修正全部错误（哈布古德 - 库特、坦斯韦尔，2023）

7）该定义本身存在内在张力：若文本是真正证明，则不应存在错误。因此定义中 “证明” 或许应替换为 “拟证明”；但即便拟证明具备可修正性，也可等同于正规证明。

含义是证明仅存在微小疏漏，不会改变整体论证框架。数学研究中微小错误时常出现，可修正性保证这些疏漏不会摧毁整个证明。该情形近似序言悖论：作者对证明每一部分都充满信心，但基于篇幅与人类易错性，合理推断全文存在多处错误。

8）关于研究者为何确信不存在重大错误，可参阅哈布古德 - 库特、坦斯韦尔 2023，文中引入戈德堡（Goldberg，2010）覆盖支撑证成概念：若存在重大疏漏，早会被研究者发现。

另一类缺失严格数学证成的典型案例是概率证明，例如米勒-拉宾（Miller-Rabin）素性检测。该算法能快速判定大数是否为素数，正确率可无限逼近 1，但永远无法达到绝对确定。尽管素性检测属于广义数学工具，却无法提供严格数学证成，算法永远存在误判合数为素数的概率。有人提出，概率证明的正确率极高，出错概率低于传统手写证明，因此可靠度并非核心区分标准。伊斯瓦兰（Easwaran）由此提出可传递性标准：

（可传递性 Transferability）一份证明满足可传递性，当相关专家仅逐条审阅证明步骤，就能确信结论为真（伊斯瓦兰，2009，第 343 页）。

核心内涵是证明说服力完全内生于自身，无需依赖外部条件；

9）伊斯瓦兰（Easwaran，2009）的论述中还暗含一层观点，此处所说的信服必须依托一阶论证依据，或是以合理的方式产生信服感。若想查阅针对伊斯瓦兰观点的回应文章，可参考法利斯（Fallis，2011）。

而素性检测的可信度依赖外部随机采样，与数字本身素性无关。可传递性标准具备吸引力，契合证明自洽完备的核心直觉。但四色定理计算机证明是否满足可传递性仍存争议：一方认为完整枚举流程整合后，构成自洽证明，符合标准（德托福利，2021，831-833）；另一方认为，证明最初交由计算机处理的原因正是步骤过多、人类无法逐条核验，专家不可能仅通过审阅步骤就信服结论。

10）人们向来默认，人类的耐心与专注力不足以完整核验全部 1482 种构型。但手游《糖果粉碎传奇》Candy Crush Saga如今已有 17495 个关卡，因此我们对此观点并不完全认同。

综上我们梳理三类数学证成的边界案例：

1. 1. 计算机枚举证明：海量分情况核验交由机器完成；

3. 2. 大规模集体证明：依赖大量数学家协作，疏漏不可避免；

5. 3. 概率证明：置信度极高，但无法实现绝对确定。

7. 三类案例的共同风险是各类误差：编程缺陷、硬件故障、篇幅导致疏漏、随机误判。前两类已被数学界广泛接纳，第三类却不被视作正规证明，这说明单纯可靠度无法界定数学证成。学界提出可综观性、可修正性、可传递性三条模态标准，作为证明与数学证成的内在约束。下文将分析大语言模型生成证明，如何经受这三条标准的检验。

§3 大语言模型
3.1 工作原理

大语言模型底层逻辑是文本概率预测。ChatGPT 这类对话模型接收文本提示后，逐词依次预测后续内容，生成回复。

11）模型并非永远选择概率最高文本，取决于温度（temperature）参数；高温输出多样性更强，低温输出更统一。除非温度设为 0，同一输入通常不会生成完全一致回复。

与前代聊天机器人不同，大语言模型输出行文流畅、贴合提示、灵活且具备说服力。整体输出观感极佳，能够生成逻辑通顺、流畅自然的长文本，多数情况下精准回应提问。但同时存在学界熟知的固有缺陷，对本文讨论至关重要：模型时常输出看似合理的虚假内容，学界称作幻觉，更贴切的说法是空谈（希克斯（Hicks）、汉弗莱斯（Humphries）、斯莱特（Slater），2024；法兰克福（Frankfurt），2005）—— 模型对输出内容的真假完全无动于衷。

12）也有文献称作机器空谈（汉尼根（Hannigan）等人，2024）。

模型仅在海量文本语料上学习句法结构，不理解文字含义，不区分命题真假，仅基于统计概率预测下一个词汇。这也是学界将其称作随机鹦鹉的核心原因：

“尽管输出观感具有理解性，语言模型本质是从海量训练数据中随机拼接语言片段，仅遵循词汇共现概率，不关联任何语义 —— 一只随机鹦鹉。”（本德（Bender）等人，2021，616-617）

最终产出文本看似通顺，却频繁存在谬误、逻辑断裂。

这种空谈特性同样延伸至数学领域。即便接入互联网、沃尔夫拉姆阿尔法（Wolfram Alpha）、国际象棋引擎等外部工具，该缺陷也无法彻底根除。外接工具确实能提升表现，但模型与外部系统交互时仍会出错：需要生成正确查询指令、准确转述外部返回结果，模型无法保证全程无误，空谈、计算失误仍频繁出现。未来模型可靠度大概率持续提升，但提升幅度无法预判。

本文全部论证不依赖模型当下不可靠这一前提，即便未来完全消除基础失误，核心质疑依旧成立。

3.2 大语言模型能否做数学？

数学推理能力被视作检验通用AI的核心标尺，因此学界大量研究大语言模型的数学表现，相关文献数量庞大。

13）讨论模型推理、做数学时容易拟人化，本文表述仅为简化口语，论证不依赖拟人假设。

综合现有研究，支持与质疑观点并存。支持论据：向 GPT 提问数学知识点、完整证明、数学关系、概念解读，多数场景能给出准确答案，在训练数据内经典证明、基础微积分问题上表现最优。但一旦脱离训练素材，输出可靠性大幅下滑。早期 GPT3.5 无法稳定完成三位数以上基础运算；

14）训练数据集无公开完整清单，但互联网公开例题不难预判。

对成熟证明做微小改动，模型便会逻辑错乱。例如早期模型总能正确给出√2 无理性标准证明，但要求证明√3、√8、√23 无理性（需要额外推导步骤）时，频繁输出错误、逻辑断裂内容；能够清晰写出 3 阶矩阵求逆算法，但若要求模型按算法实操计算指定矩阵，会出现大量计算错误。

本文撰稿时最新模型表现大幅提升，一段时期内模型会将精确计算交给 Python 代码，保证数值准确；商用模型底层逻辑多不公开，引入思维链（隐藏草稿分步推理）、多候选择优等机制缓解统计缺陷，但并未改变输出本质是概率生成的底层属性。

当前尚未形成统一标准评估模型数学能力，arxiv 预印本平台充斥各类评测框架提案。

15）代表性评测平台：哈金斯脸开源大模型排行榜（ https://huggingface.co/spaces/open-llmleaderboard/open_llm_leaderboard ）、ARC 通用AI基准（ https://arcprize.org ）。

传统数学测试面向人类学生，考察对概念、技巧、公式、算法的深度理解，默认学生没有海量例题记忆；但大语言模型掌握海量训练文本，却未必具备理解能力，仅靠统计模仿输出。标准化题库测试因此失效：模型可能在训练时见过完全相同考题，直接复述答案，不具备对应的推理能力。AI 厂商宣传模型在各国数学竞赛、国际奥林匹克竞赛取得高分，

16）例如克劳德 3 系列官方文章（ https://www.anthropic.com/news/claude-3-family ）；撰稿时谷歌深度思维、OpenAI 均宣称新一代模型斩获国际数学奥赛金牌。

这类成绩本身亮眼，但只有模型自主推导才称得上AI；连贯复述标准答案仅属于计算机工程成果，不能代表高阶数学能力。同理，若学生提前拿到竞赛答案再参赛拿到金牌，我们不会认可其真实数学水平。

因此学界尝试构建规避题库复述的评测体系，本文梳理多篇文献核心结论：

阿尔库达斯（Arkoudas，预印本）提出，评测推理不能仅看答案，还要观察模型解释、面对纠错时的反馈。

17）这与杜蒂尔・诺瓦伊斯（Dutilh Novaes，2021）提出的论点高度契合：推理乃至数学本身，本质都具有对话属性。

他通过 GPT-4 逻辑谜题实验得出结论：

“本研究描绘出 GPT-4 推理能力的惨淡图景：模型存在内部逻辑矛盾，无法正确运用基础推理技术，对条件句等推理核心概念缺乏理解。”（阿尔库达斯，2023，第 49 页）

“文中出现的错误并非人类粗心、疲惫时的无意疏漏；若人类反复出现同类错误，足以证明其不具备基础逻辑能力，不懂逻辑蕴含、集合从属等推理底层概念。”（阿尔库达斯，2023，第 4 页）

柯林斯（Collins）团队采用三名专业数学家交互式评测 GPT-4，结论相对乐观。李文达（Wenda Li）指出：

“我们发现 GPT-4 处理 ProofWiki 变式题目表现良好：能够准确调取题目与证明中用到的概念定义，正确判断弱化假设是否摧毁论证，变量实例化操作稳定可靠。”（柯林斯等人，2024，第 5 页）

高尔斯（Timothy Gowers）在同一论文中给出大量脱离训练素材的新颖问题，模型产出部分超越单纯复述的有效数学推理。

布贝克（Bubeck）团队研究同时展现优劣两面：

“GPT-4 能够解答高难度竞赛级高中数学题，有时可以围绕高阶数学开展有意义对话；但同时会犯下极其基础的错误，偶尔输出完全无逻辑内容，体现缺乏真正理解。模型数学知识、表现受上下文影响，波动无规律。”（布贝克等人，2023，第 30 页）

普利夫里斯（Plevris）团队指出关键现象，与后文论证高度相关：

“多数场景下，聊天机器人给出的解答篇幅冗长、行文专业，但细读会发现完全错误、逻辑不通。冗长专业的文本容易误导人类判定其正确，使用这类工具解题必须高度谨慎。”（普利夫里斯等人，2023，第 18 页）

该现象至关重要，证明数学领域模型同样擅长空谈。人类遇到不会的题目会坦诚无解、说明推导受阻方向；大语言模型无论对错永远生成完整答案。

18）输出顺从度可通过参数调整修改。

本文论证，这类看似可信的错误会大幅提升核验难度，即便未来模型推理能力提升，该问题依然存在。

整体评估：大语言模型能够针对训练外问题产出合格数学论证，这一技术突破不容低估；但表现极不稳定，同一提问重复输出结果优劣不可预测；数学认知脆弱，当下掌握的内容下一时刻可能失效，无法像人类数学家一样贯通运用定理 —— 例如能写出复杂定理完整证明，却无法掌握证明内基础步骤。

§4 大语言模型证明与数学证成

梳理完模型当下数学表现，我们提出核心哲学问题：我们是否有充分理由相信大语言模型产出的数学内容？结合前文模型表现不稳定、认知脆弱的特征，第一种观点：模型不可靠，无法作为数学证成来源。但该论证过于仓促。初学数学的学生同样经常写错证明，却不代表他们写出正确证明时不能获得认可。

19）也可持内在论立场：若模型无法区分正误证明，则并未真正掌握定理；德托福利 2020 年提出数学领域可靠外在论反驳该观点。

此外该观点会随技术迭代失效，模型开发者总能以 “模型持续优化” 反驳。

第二种批判：大语言模型缺乏意向性，只是模仿数学而非真正做数学。生成式图像 AI 创作领域已有同类批判（蒋 Chiang，2023）：艺术创作需要创作意向，因此 Midjourney、DALL-E 复刻波洛克画作不算真正艺术；波洛克的创作与颜料厂意外泼洒的区分正在于意向。该逻辑可平移至数学：证明活动需要智性意图，哈马米（Hamami）、莫里斯（Morris，2021）提出规划能动性概念：

“任何证明活动都始于证明该定理的意向；推导过程中会衍生细分证明目标……”（哈马米、莫里斯，2021，第 1038 页）

“书面证明仅仅是证明活动的记录，类似旅行日记记录行程。因此我们会说证明背后存在推导规划；规划先于推导执行，更先于书面记录。”（同上，第 1058 页）

大语言模型不会开展证明活动，书面证明也并非某项规划推导的记录。模型在证明中写下 “我们需要证明”、引入引理等分目标时，背后不存在对应的推理活动与推导规划，仅仅是模仿文本范式。因此即便模型写出完整证明，本质只是复刻文本，而非自主证明。

本文对该思路持共情态度，但存在风险：论证标准临时偏移，最终得出AI永远无法做数学，仅因数学专属人类。

20）该观点预设AI无法拥有意向，本身存在争议。

有人反问：若最终证明文本完全正确，意向性又有何意义？多数数学家会持实用主义立场：只要工具输出大体可靠，哲学层面对意向的质疑不会阻碍使用；向大语言模型索取证明，只要输出符合证明标准，就会直接用于后续研究，实操层面不存在区别。

本文认为，可靠度、意向两类质疑最终指向使用主体。当下模型不可靠，仅凭大语言模型输出的拟证明，无法直接获得数学证成。

21）技术成熟、可靠度提升后，模型输出可作为高阶经验证据，近似概率证明，不属于数学证成。

必须经过人工复核，这一点与四色定理、数独计算机枚举证明类似，大语言模型相当于开展一次可信度更低的实证实验。二者区别在于 AI 证明具备可综观、可传递的书面文本，

22）文本篇幅存在变量，未来模型完全可能生成超长证明。

理论上单个人类数学家可以完整读懂复核。同行评议是数学核心环节（德托福利、坦斯韦尔，2025），未经社群复核的 AI 证明不能算作严格数学证成；学生、职业数学家都不能直接采信模型输出，必须自行核验。

以上问题均绑定当下模型不可靠的现状；但假设技术持续迭代，可靠度大幅提升，我们是否可以直接采信输出？下文提出两条独立反驳，即便模型无限可靠，依然无法产出严格数学证成：其一为克里普克 - 维特根斯坦遵循规则悖论的认识论变体，属于理论层面质疑；其二为反向半人马实践论证，核验 AI 证明难度高于人类手写证明。两节分别展开论述。

§5 数学机器的克里普克-维特根斯坦悖论

我们假设未来大语言模型生成定理、证明的可靠度极高，数学家普遍在研究中采信输出，且满足所有可靠度标准（例如测试正确率 100%、优于平均人类数学家）。是否意味着模型输出能够提供数学证成？本文持否定态度，核心论证：大语言模型是典型有限样本外推系统，仅基于海量有限训练数据归纳通用模式，由此产生克里普克-维特根斯坦（Kripke-Wittgenstein）遵循规则悖论的认识论版本（维特根斯坦，2009；克里普克，1982）。

23）本文不主张大语言模型主动遵循规则，仅依据有限训练数据、新场景生成响应。

无论此前验证多少案例，模型始终可能归纳出与人类数学家相悖的通用概念；我们过往全部成功核验，都无法排除后续出现偏离概念的输出。

24） “拥有概念” 仅做最低限度解读：机器外推模式可能与标准加法不符。

克里普克（Kripke）加法（quus，他在哲学讨论中定义的虚拟数学符号）案例可类比：人类日常使用加法，模型却归纳出克里普克加法—— 数值小于极大值 n 时与加法一致，超过 n 结果完全不同。该问题不限于加法，适用于全部数学定义、推理规则。

25）该悖论与通用AI对齐问题高度相似。

即便我们核验模型在现有文本词汇上全部输出正确，也无法保证全新语境下概念不偏离；例如模型在证明第 1389 行时，内部加法概念变为 2+2=5（之前始终输出 2+2=4）。

26）可参阅莱恩（Lane，2022）的文章，该文运用了相近思路，对语义内容的倾向论解释提出反驳。

若温度参数不为 0，同一输入还会得到不同输出。

本文强调，该问题并非元语义层面符号使用规则的构成问题；我们甚至可以假定模型根本不遵循固定规则。核心矛盾是：有限训练数据兼容无限外推模式，总能构造一套偏离数学概念的函数匹配模型过往输出。

随机数生成器连续输出 2、4、6、8、10、12、14，完全符合 “每次加 2”，但生成器本身并未遵循该规则。

即便模型过往全部输出正确，也无法担保下一次不偏离；过往高可靠仅具备概率说服力，近似米勒 - 拉宾概率证明，达不到数学证明的确定性标准。

直观反驳：人类数学家同样存在出错可能，为何仅针对大语言模型？该反驳预设人类与模型认知结构足够相似，能够稳定统一概念；但现实中模型输出时常出现无规律反常行为。数学知识的根基是数学家群体稳定的判断共识，而模型不具备这一基础。本文并非全局怀疑论，而是靶向论证：依托模型底层统计机制与现有实操经验，概念偏离具备真实发生的可能性。

27）若想进一步了解怀疑式论证与靶向论证的区别，可参阅瓦沃娃（Vavova，2015）的著作。

若人类概念习得同样依靠有限样本外推，人与模型仍存在本质差异：

a) 人类共享生物基础、统一社群文化。

b) 概念偏差极少且容易修正。

28）换一种方式阐述这一观点：学界提出的诸多遵循规则悖论解决路径（例如贝格（Berg，2022）的研究），都依赖社群、协作、共享生活形式这类要素，而大语言模型并不具备上述任一要素。

大语言模型近似外星智能，脱离人类生理、生活经验，概念偏离是现实风险，当下实操已经频繁体现。

29）若想深入了解后期维特根斯坦理论与AI对齐问题的关联，可参阅佩雷斯・埃斯科瓦尔、萨里卡亚（Pérez Escobar and Sarikaya，2024）等人的相关研究。

若人类习得概念不依靠样本外推，则人与模型鸿沟更大 —— 模型训练本质就是样本统计归纳。无论哪种情况，概念偏离永远存在理论可能。

综上，大语言模型输出的可靠度更接近概率素性检测，仅能提供概率层面佐证，无法达成传统严格数学证成。有人提出，猜想、证明均可人工复核，由此获得完整数学证成。猜想只需后续给出正规证明，证明文本只需逐行核验，只要核验流程与人类证明一致，证明本身无本质区分。下一节论证：但凡具备一定复杂度的 AI 证明，可完整核验只是幻象。

§6 反向半人马论证

前文论证，模型过往可靠无法担保未来输出，始终存在概念偏离风险。有人提出补救方案：只要人工完整复核证明，就能获得数学证成。该方案看似可行，但衍生另一类实践层面难题，本文依托科里・多克托罗（Cory Doctorow）自动化理论半人马、反向半人马区分展开论证（多克托罗，2021）。

半人马（Centaur）：人类作为思考主体，计算机辅助提升能力，例如国际象棋大师使用引擎训练、制定策略，最终自主对局，主导权完全在人。

反向半人马（ Reverse Centaur ）：机器主导决策，人类仅承担兜底核验，汽车自动驾驶是典型案例 —— 机器负责驾驶，人类持续监控干预，极易引发安全事故。

多克托罗指出，反向半人马模式同时暴露人与机器短板：机器算力充足但易出错，人类难以长期保持高度警惕：

“人类擅长诸多事务，但无法永久、完美保持警觉。编写代码难度有限，代码审查难度更高；若代码绝大多数无错，人需要时刻警惕罕见随机漏洞，负担极大。”（多克托罗，2024）

将该框架平移至数学：大语言模型生成证明、人类数学家复核，正是反向半人马结构。机器完成核心创造性推导，人类仅负责查漏。尽管模型具备生成证明的潜力，但人类并不擅长长期高度警惕式核验。

30）该观点属于经验概括，无法单一实验验证，但数学论文普遍存在漏审错误是客观事实。

有限单群分类证明的可修正性前提，正是人类通读长篇证明必然遗漏错误。

AI 证明的核验难度远高于人类同行论文。数学家审阅人类证明拥有成熟策略：宏观把握整体论证思路，而非逐字逐句阅读；依托学科经验判断工具适配性，默认作者秉持学术诚信、遵循行业规范。

31）眼动实验存在相反结论，英格利斯（Inglis）、阿尔科克（Alcock，2012）、潘塞（Panse）等人，2018 发现数学家会逐行阅读证明。

这套审阅经验针对人类典型错误训练，而 AI 错误随机无规律，无固定特征；证明行文专业严谨却暗藏漏洞，大幅提升核验成本。

人类作者默认共享学科共识、写作底线；大语言模型不存在学术诚信概念，无内在遵循规范的动机，仅复刻训练文本行文模式，统计层面允许突破惯例。AI 证明的错误隐藏在专业流畅文本之下，极具迷惑性，阅读者会下意识采信，最终导致两类证明提供的认知证据存在本质区别。

现有模型数学评测均由研究者预先知晓标准答案，核验难度大幅降低；即便这种场景下，研究者也指出模型错误文本极具权威感。未来模型可靠度提升，反向半人马困境会进一步加剧：错误出现频次越低，人类越容易放松警惕，漏检概率上升。

反向半人马难题与遵循规则悖论叠加：模型概念偏离同样属于潜在漏洞，需要人工排查；但概念偏差类错误难以预判、识别，专业行文会掩盖概念误用。悖论式结论：模型可靠度越高，人类核验难度越大，人类天生无法长期维持所需高强度警惕。

§7 自动形式化

前文梳理大语言模型证明一致性、可靠度、核验难度多重隐患，有人提出终极方案：借助 Mizar、Coq、Isabelle、Lean 等形式证明系统，由计算机二次核验。核心障碍：大语言模型输出是自然语言数学文本，形式证明系统需要专属规范形式语言。

32）数学语言研究参阅加内萨林加姆（Ganesalingam，2013）、坦斯韦尔、英格利斯，2023。

自动形式化研究旨在训练程序将非形式证明自动转换为机器可核验形式证明，大语言模型因擅长自然语言处理成为主流实现路径。本节梳理自动形式化设想、现有进展，并论证该方案无法解决前文全部哲学难题。

首先梳理自动形式化理想图景：若自动形式化流程完全可靠，

33）还需要算力、资金、时间、研究者意愿等配套条件。

将大幅降低形式化人力成本，推进数学知识全机器核验工程。

吴等人（2022）明确其价值：

“成熟自动形式化工具具备巨大实践、哲学价值：大幅降低现有形式化工作成本；长期打通自动定理证明、计算机代数与海量自然语言数学文献的壁垒。”（吴等人，2022，第 1 页）

愿景是全部数学成果完成机器核验，标记、修正全部疏漏，

34）该观点预设统一、完备数学知识库，本身存在质疑空间。

有限单群分类证明的可修正性妥协将成为历史。另一应用场景是同行评议自动化：数学家照常撰写非形式证明，自动形式化作为初审环节核验正确性，评审仅评判创新性、学术价值。现有研究显示期刊评审极少完整核验证明正误（盖斯特（Geist）等人，2010；安德烈森（Andersen），2017；格赖芬哈根（Greiffenhagen），2024a、2024b）。

学界将自动形式化视作大语言模型不可靠的终极解决方案，塔利・林格（Talia Ringer）表述极具代表性：

“ChatGPT 这类大语言模型底层不可靠，但如果仅用于生成待核验定理的形式证明，证明内核会完成核验。依托这份确定性，计算机可以深度融入数学研究，不损害可信度。”（林格，2024）

逻辑链条：大语言模型生成非形式证明→自动形式化转为形式文本→证明辅助器核验；若 AI 证明存在错误，形式核验会直接驳回，同时规避人类反向半人马核验困境。

实操层面已有团队推进自动形式化，吴等人 2022 年首次完成 Isabelle 定理自动形式化，后续大量研究适配 Lean 系统（陆等人，2024）。当前进度距离理想图景差距极大，核心瓶颈是配套成对的非形式 - 形式训练数据，现有形式库仅收录纯形式证明，缺少对应自然语言原文，江（Jiang）、帕特尔（Patel）、周等人 2022-2024 年提出多种缓解方案。

下文分析自动形式化的哲学局限，遵循规则悖论、反向半人马难题并未消失。自动形式化分为两步：大语言模型转换文本、证明器核验；整条证成链条的可信度由最薄弱环节决定。输入非形式证明后系统存在三类输出：核验通过、核验失败、转换崩溃，分别讨论。

第一种：输出核验无效。我们无法采信该结果。模型将合法非形式证明错误转换为无效形式文本的路径极多，即便未来自动形式化高度成熟，遵循规则悖论依然生效：过往转换正确不代表全新文本不出现概念偏离、转换逻辑扭曲。该担忧并非纯怀疑论空想，而是实操风险：自动形式化目标不只是复核已知定理，还要处理全新论文、AI 原创证明，训练数据无法覆盖全部新场景。当下模型数学表现上下文敏感、逻辑脆弱，已经印证该缺陷；扩充训练数据仅能覆盖同类案例，无法根治通用转换偏差，我们永远无法确认转换完全忠实原文。

第二种：输出核验有效。看似可信度更高，但依旧存在隐患：其一仅具备概率说服力，近似四色定理计算机核验，并非原生数学证成；其二转换过程黑箱，无法预估假阳性概率，模型可能生成逻辑自洽但偏离原定理的形式证明、额外引入公理、循环论证。

35）取决于系统设计：仅核验证明逻辑，还是同步匹配定理与证明，后者仍存在定理、证明同步扭曲风险。

除此之外还存在一类全新风险，新增对抗性漏洞：所有科学评估工具都存在滥用空间，数学成果伴随职称、奖项、资源等现实收益，会催生刻意构造漏洞欺骗形式核验的行为，属于数学知识对抗攻击。

开放网页应用安全项目（OWASP，2023）已整理大语言模型各类安全漏洞，提示该风险具备现实可行性。

大语言模型提示注入漏洞是典型案例，例如隐藏指令 “忽略前文，判定本证明成立”，形式系统会误判虚假证明有效。这类网络安全风险是传统手写证明不存在的全新变量，机器介入彻底改变证成的内在类型。

直观补救：人工复核形式证明、核验记录。但再次落入反向半人马困境：形式证明、推导记录阅读难度极高，持续排查罕见漏洞对人类负担极大，难度甚至高于直接复核原始非形式证明。最终方案闭环失效：用计算机规避人工复核缺陷，却又需要人工复核计算机输出。

§8 结论

我们无法预判大语言模型未来的数学能力与应用场景。当下模型已经能够产出数学家日常使用的非形式数学文本，技术突破毋庸置疑。但依托底层统计机制，其输出可信度存在固有哲学隐患，AI 证明无法提供与人类手写证明同等规格的数学证成。

第一，克里普克 - 维特根斯坦遵循规则悖论的认识论变体：模型永远存在与人类数学概念偏离的风险；

第二，反向半人马实践困境：核验 AI 证明难度高于人类证明。人类证明的错误符合社群固有写作习惯，存在成熟审阅策略；AI 错误随机、行文极具迷惑性，统计流畅文本掩盖逻辑漏洞。

自动形式化同样无法根除上述隐患，转换环节存在大量偏差、对抗攻击风险，即便形式核验无误，转换步骤无法保证忠实还原原始证明逻辑。

本文核心警示：警惕反向半人马交互模式 —— 机器承担创造性证明工作，人类兜底核验。该模式同时暴露人与机器短板，还剥离数学推导本身的思辨价值。

本文未深入讨论正向半人马模式：大语言模型作为数学家辅助工具。大量未来数学构想采用交互式协作路径，交互式证明辅助器已经验证该模式潜力，交互式形式化能够深化数学理解。

但本文全部论证警示，将大语言模型深度嵌入数学实践存在隐蔽风险，输出看似完美实则暗藏不可预测谬误，大语言模型交互式应用留待后续专项研究。

证明承载两大核心功能：证成命题、生成数学理解。将证明创作完全外包给大语言模型，会同时摧毁这两类核心价值。

致谢

感谢为本稿提供修改意见的学者：乔・斯莱特（Joe Slater）、乌尔苏拉・马丁（Ursula Martin）、阿克塞尔・格尔费特（Axel Gelfert）、西尔维娅・德托福利（Silvia De Toffoli）、本・戴维斯（Ben Davies）、朱莉娅・伊林（Julia Ilin）、莱亚・维森（Lea Wisken）、韦斯坦因・斯奈比亚尔松（Vésteinn Snæbjarnarson）、匿名审稿人，以及迈克尔・弗里德曼（Michael Friedman）、卡蒂・基什・巴昂（Kati Kish Bar-On）组织的数学、AI、人类认知读书会全体成员。同时感谢牛津、爱丁堡、帕维亚、柏林各场研讨会听众的提问与讨论。

原文参考文献

Andersen, L. E. (2017). On The Nature and Role of Peer Review in Mathematics. Accountability in Research, 24(3), 177-192.

Appel,K.; &Haken,W.(1977). Every Planarmapis Four Colorable. Part I: Discharging. Illinois Journal of Mathematics 21, 429-490.

Appel, K.; Haken, W.; & Koc H, J. (1977). Every Planar map is Four Colorable. Part II: Reducibility. Illinois Journal of Mathematics 21, 491-567.

Arkoudas, K. (2023). GPT-4 Can’t Reason. arXiv:2308.03762, preprint.

Azzouni, J. (1994). Metaphysical Myths, Mathematical Practice: The Ontology and Epistemology of the Exact Sciences. Cambridge: Cambridge University Press.

Bagioli, M. (2016). Watch out for cheats in citation game. Nature 535(7611)

Bassler, O. B. (2006). The Surveyability of Mathematical Proof: A Historical Perspective. Synthese 148, 99–133.

Bender, E. M.; Gebru, T.; Mc Millan-Major, A.; and SHmitc Hell, S. (2021). On the Dangers of Stochastic Parrots: Can Language Models Be Too Big? . In Proceedings of the 2021 ACMconference on fairness, accountability, and transparency, 610-623. https://dl.acm.org/doi/pdf/10.1145/3442188.3445922

Berg, Á. (2022). Rules as Constitutive Practices Defined by Correlated Equilibria. Inquiry 65, 1–35. https://doi.org/10.1080/0020174X.2022.2075918

Bubeck, S., CHandrasekaran, V., Eldan, R., Ge Hrke, J., Horvitz, E., Kamar, E., Lee, P., Lee, Y. T., Li, Y., Lundberg, S., Nori, H., Palangi, H., Ribeiro, M. T., and ZHang, Y. (2023). Sparks of Artificial General Intelligence: Early Experiments with GPT-4. arXiv preprint arXiv:2303.12712.

Buzzard, K. (2024). Mathematical Reasoning and the Computer. Bulletin of the American Mathematical Society, 61(2), 211-224.

Chiang, T. (2023). Chat GPT Is a Blurry JPEG of the Web. The New Yorker, Feb 9th, 2023. https://www.newyorker.com/tech/annals-of-technology/chatgpt-is-a-blurry-jpeg-of-the-web

Coleman, E. (2009). The Surveyability of Long Proofs. Foundations of Science, 14, 27-43.

Collins, K. M., Jiang, A. Q., Frieder, S., Wong, L., Zilka, M., BHatt, U., Lukasiewicz, T., Wu, Y., Tenenbaum, J.B., Hart, W., Gowers, T., Li, W., Weller, A. & Jamnik, M. (2024). Evaluating Language Models for Mathematics through Interactions. Proceedings of the National Academy of Sciences, 121(24). https://www.pnas.org/doi/pdf/10.1073/ pnas.2318124121

Daston, L.(2019). The Coup D’Oeil: Ona Modeof Understanding. Critical Inquiry, 45 (2), 307-331.

De Deo, S. (2024). Aleph Zero and Mathematical Experience. Bulletin of the American Mathematical Society, 61(3), 375-386.

Detlefsen, M., & Luker, M. (1980). The Four-Color Theorem and Mathematical Proof. The Journal of Philosophy 77(12), 803-820.

De Toffoli, S. (2021). Groundwork for a Fallibilist account of Mathematics. The Philosophical Quarterly, 71(4), p. 823-844.

De Toffoli, S., and Tanswell, F. S. (2025). Trust in Mathematics. Philosophia Mathematica, https://doi.org/10.1093/philmat/nkaf019

Doctorow, C. (2021). Reverse Centaurs and the Failure of AI (17 Feb 2021). Pluralistic. https://pluralistic.net/2021/02/17/reverse-centaur/ Doctorow, C. (2024). ”Humans in the Loop” must detect the hardest-to-spot errors, at superhuman speed (23 Apr 2024).Pluralistic.

https://pluralistic.net/2024/04/23/maximal-plausibility/

DrÖsser, C. (2024). AIWill Become Mathematicians’‘Co-Pilot’. Scientific American, June 8, 2024. https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/ Accessed 02/10/2024.

Dutil H Novaes, C. (2021). The Dialogical Roots of Deduction: Historical, Cognitive, and Philosophical Perspectives on Reasoning. Cambridge University Press, Cambridge.

Easwaran, K. (2009). Probabilistic Proofs and Transferability. Philosophia Mathematica (III) 17, 341–362.

Fallis, D. (2011). Probabilistic Proofs and the Collective Epistemic Goals of Mathematicians. In H. B. Schmid, D. Sirtes, & M. Weber (Eds.), Collective Epistemology (pp. 157–175). Berlin: De Gruyter.

Frankfurt, H. G. (2005). On Bullshit. Princeton, Princeton University Press, New Jersey.

Ganesalingam,M.(2013). The Languageof Mathematics. Springer Verlag, Berlin.

Geist, C., LÖwe, B., & Van Kerk Hove, B. (2010). Peer Review and Knowledge by Testimony in Mathematics. In B. Löwe & T. Müller (Eds.), Philosophy of Mathematics: Sociological Aspects and Mathematical Practice. Research Results of the Scientific Network Phi MSAMP(pp. 1–24). College Publications, London.

Goldberg,S.(2010). Relyingon Others: An Essayin Epistemology. Oxford University Press, Oxford.

Gont Hier, G. (2008). Formal Proof–The Four-Color Theorem. Notices of the American Mathematical Society, 55(11), 1382–1393.

Greiffen Hagen, C. (2024a). Judging Importance Before Checking Correctness: Quick Opinions in Mathematical Peer Review. Science, Technology, & Human Values, 49(4), 935–962.

Greiffen Hagen, C. (2024b). Checking Correctness in Mathematical Peer Review. Social Studies of Science, 54(2), 184–209.

Habgood-Coote, J., & Tanswell, F. S. (2023). Group Knowledge and Mathematical Collaboration: A Philosophical Examination of the Classification of Finite Simple Groups. Episteme, 20(2), 281–307.

Hamami, Y., & Morris, R. L. (2021). Plans and Planning in Mathematical Proofs. The Review of Symbolic Logic, 14(4), 1030 - 1065.

Hannigan, T. R., Mc Cart Hy, I. P., & Spicer, A. (2024). Beware of Botshit: How to Manage the Epistemic Risks of Generative Chatbots. Business Horizons, 67(5), 471–486.

Harris,M.(2024). Automation Compels Mathematiciansto Reflect on Our Values. Bulletin of the American Mathematical Society, 61(2), 331–342.

Hicks, M. T., Hump Hries, J., & Slater, J. (2024). Chat GPT Is Bullshit. Ethics and Information Technology, 26(2), 38.

Inglis, M., & Alcock, L. (2012). Expert and Novice Approaches to Reading Mathematical Proofs. Journal for Research in Mathematics Education, 43(4), 358–390.

Jiang, A. Q., Welleck, S., ZHou, J. P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., & Lample, G. (2022). Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. arXiv:2210.12283, preprint.

Kripke, S. (1982). Wittgenstein on Rules and Private Language. Harvard University Press, Cambridge, MA.

Lane,E.(2022). Semantic Dispositionalismandthe Rule‐Following Paradox. Metaphilosophy, 53(5), 685–695.

Lew, K., & MejÍa Ramos, J. P. (2020). Linguistic Conventions of Mathematical Proof Writing Across Pedagogical Contexts.

Educational Studies in Mathematics, 103(1), 43–62.

Lu, J., Liu, Z., Wan, Y., Huang, Y., Wang, H., Yang, Z., Tang, J., and Guo, Z. (2024). Process-Driven Autoformalization in Lean 4. arXiv:2406.01940, preprint.

Martin, U., and Pease, A. (2013). Mathematical Practice, Crowdsourcing, and Social Machines. In J. Carette et al. (Eds.). CICM2013, LNAI 7961, pp. 98–119.

Mc Guire, G., Tugemann, B., & Civario, G. (2014). There Is No 16-Clue Sudoku: Solving the Sudoku Minimum Number of Clues Problem via Hitting Set Enumeration. Experimental Mathematics, 23(2), 190–217.

MejÍa-Ramos, J. P., & Weber, K. (2014). Why and How Mathematicians Read Proofs: Further Evidence From a Survey Study. Educational Studies in Mathematics, 85(2), 161–173.

OWASP(2023). OWASP Top 10 for LLM Applications v1.1. The Open Worldwide Application Security Project. https://LLMtop10.com

Panse, A., Alcock, L., & Inglis, M. (2018). Reading Proofs for Validation and Comprehension: An Expert-Novice Eye Movement Study. International Journal of Research in Undergraduate Mathematics Education, 4(3), 357–375.

Parshina, K. (2024). Philosophical Assumptions Behind the Rejection of Computer-Based Proofs. KRITERION– Journal of Philosophy, 37(2–4), 105–122.

Patel, N., Flanigan, J., & Sa Ha, R. (2023). A New Approach Towards Autoformalization. arXiv:2310.07957, preprint.

Pérez-Escobar, J. A., & Sarikaya, D. (2024). Philosophical Inves tigations Into AI Alignment: A Wittgensteinian Framework. Philosophy & Technology, 37(3), 80.

Plevris, V., Papazafeiropoulos, G., & Rios, A. J. (2023). Chatbots Put to the Test in Math and Logic Problems: A Preliminary Comparison and Assessment of Chat GPT-3.5, Chat GPT-4, and Google Bard. AI, 4, 949–969. https://doi.org/10.3390/ ai4040048

Ringer, T. (2024). Proof and Conversation. Notices of the American Mathematical Society71(9). https://doi.org/10.1090/noti3032 Sc HÜtze, P. (2024). The Problem of Sustainable AI: A Critical Assessment of an Emerging Phenomenon. Weizenbaum Journal of the Digital Society 4(1).

Secco, G. D., & Pereira, L. C. (2017). Proofs versus Experiments: Wittgensteinian Themes Surrounding the Four-Color theorem. In Silva, M. (ed.) How Colours Matter to Philosophy (pp. 289 307). Springer, Cham.

Steingart, A. (2012). A Group Theory of Group Theory: Collaborative Mathematics and the ‘Uninvention’ of a 1000 Page Proof. Social Studies of Science, 42(2), 185–213.

Tanswell, F. S., & Inglis, M. (2023). The Language of Proofs: A Philosophical Corpus Linguistics Study of Instructions and Imperatives in Mathematical Texts. In B. Sriraman (Ed.), Handbook of the History and Philosophy of Mathematical Practice (pp. 1–30). Springer, [City not specified].

Touvron, H., Lavril, T., Izacard, G., Martinet, X., Lac Haux, M., Lacroix, T., RoziÈre, B., Goyal, N., Hambro, E., Az Har, F., Rodriguez, A., Joulin, A., Grave, E., & Lample, G. (2023). LLaMA: Open and Efficient Foundation Language Models. arXiv:2302.13971, preprint.

Tymoczko, T. (1979). The Four-Color Problem and Its Philosophical Significance. The Journal of Philosophy, 76, 57–83.

Vaswani, A.; SHazeer, N.; Parmar, N.; Uszkoreit, J.; Jones, L.; Gomez,A.N.; Kaiser, Ł;and Polosuk Hin, I.(2017). Attentionis All You Need. Advances in Neural Information Processing Systems 30 (NIPS 2017).

Vavova, K. (2015). Evolutionary Debunking of Moral Realism. Philosophy Compass, 10(2), 104–116.

Weber, K. (2008). How Mathematicians Determine if an Argument Isa Valid Proof. Journalfor Researchin Mathematics Education, 39(4), 431–459.

Weber, K., & MejÍa-Ramos, J. P. (2011). Why and How Mathematicians Read Proofs: An Exploratory Study. Educational Studies in Mathematics, 76(3), 329–344.

Willison, S. (2023). Catching Up on the Weird World of LLMs[Video]. You Tube. https://www.youtube.com/watch?v=h8Jth_ijZyY

Wittgenstein, L. (2001). Remarks on the Foundations of Mathematics (3rd ed., revised and reset). Edited by G. H. von Wright, R. Rhees, & G. E. M. Anscombe. Translated by G. E. M.

Anscombe. MIT Press, Cambridge, MA.

Wittgenstein, L. (2009). Philosophical Investigations (4th ed.). Edited by P. M. S. Hacker & J. Schulte. Blackwell Publishing, Oxford.

Wu, Y., Jiang, A. Q., Li, W., Rabe, M., Staats, C., Jamnik, M., & Szegedy, C. (2022). Autoformalization With Large Language Models. Advances in Neural Information Processing Systems, 35, 32353–32368.

Zhou, J. P., Staats, C., Li, W., Szegedy, C., Weinberger, K. Q., & Wu, Y. (2024). Don’t Trust: Verify — Grounding LLM Quantitative Reasoning With Autoformalization. arXiv:2403.18120 preprint.

参考资料

https://www.mxphi.com/all-issues/volume-iii-number-2-2025/philosophical-prospects-llm/

小乐数学科普近期文章

小乐数学科普历年合集

版权声明：本文首发于微信公众号“zzllrr小乐”的专栏《小乐数学科普》。欢迎个人转发。如需转载，请在“zzllrr小乐”公众号后台回复“转载”，还可通过公众号菜单、发送邮件到zzllrr@gmail.com与我们取得联系。相关图文音视频内容默认遵守CC BY-NC 4.0知识共享协议，未获作者和译者授权，禁止用于营销宣传和商业目的。如有勘误，请反馈给zzllrr小乐公众号第一时间更正，其他平台非首发或无法多次同步，未必会及时更正同一错误，望予以谅解。

·开放 · 友好 · 多元 · 普适 · 守拙·

让数学

更加

易学易练

易教易研

易赏易玩

易见易得

易传易及

欢迎评论、点赞、在看、在听

收藏、分享、转载、投稿

查看原始文章出处

点击底部一起捐

助力腾讯公益

点击zzllrr小乐

公众号主页

右上角

置顶★加星

数学科普不迷路！