Artificial Intelligence and the Structure of Mathematics

人工智能（AI）领域的最新进展正为数学带来变革性的能力。人们寄予厚望，认为AI将助力攻克一系列重大未解难题，并自主发现全新的数学概念。本文进一步探讨：AI如何通过开辟一条与数理逻辑互补的新路径，从而为我们理解形式证明的全局结构提供宏大的数学图景。我们首先以“普遍性证明”与“结构性超图”为框架，勾勒出数学的形式化结构，并由此引出有关数学基础结构的一系列根本性问题；继而概述实现自动化数学发现所需AI模型的核心要素，并提出一套明确的评判标准，用以衡量此类模型是否真正具备数学发现能力。当我们派遣AI智能体深入探索柏拉图式的数学世界时，我们期待它们不仅能揭示数学整体的本质，也能帮助我们辨识出那些特别契合人类认知能力的细微而精妙的数学片段。或许，它们终将为我们长久以来萦绕心头的古老命题——“数学是被发现的，还是被发明的？”——带来新的洞见；我们能否真正领悟并把握这些柏拉图式世界的地形地貌？

论文试图探索AI如何开辟一条区别于数理逻辑的新路径，以理解数学证明的全局结构与形式化基础，进而推动自动化的数学发现，并回应‘数学是被发现还是被发明’这一哲学问题。这不是传统AI for theorem proving（如形式验证或自动化推理）的技术优化问题，而是一个更具根本性的、关于数学本体论与认知结构的交叉科学问题。

将数学证明系统建模为‘结构性超图’（structural hypergraphs），并以‘普适证明’（universal proof）为抽象基元，构建可学习的、几何化与拓扑化的数学知识表征；AI代理被视作在柏拉图数学世界中自主探索的‘认知勘探者’，其轨迹揭示数学概念空间的内在连通性、密度与可理解性带（ribbons of intelligibility）。该思路跳出了符号主义与统计学习的二分法，融合形式语义、范畴结构与大模型涌现能力。

提出‘证明超图’作为统一框架，连接形式系统、范畴论与神经符号表征；定义了AI驱动数学发现的四条核心准则（可溯性、可泛化性、可解释性、可协作性）；未依赖具体定理证明任务或数据集，而是聚焦元数学结构建模；暂无公开代码或实验验证——属前瞻型概念论文；值得深入的方向包括：超图神经网络在证明空间嵌入中的应用、数学概念密度的量化度量、以及人类-AI协同发现界面的设计。

‘Language Models as Zero-Shot Reasoners over Formal Proofs’ (ICLR 2023); ‘Minerva: Solving Quantitative Reasoning Problems with Language Models’ (NeurIPS 2022); ‘A Formal Proof of the Kepler Conjecture’ (Annals of Mathematics, 2017); ‘The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics’ (2013); ‘DeepMath: Reinforcement Learning for Theorem Proving’ (AAAI 2017)