LLM将重塑数学基础设施：定理证明将变为依赖链

arankomatsuzaki · x · 2026-07-31

Aran Komatsuzaki 在讨论中指出，大语言模型（LLM）的自动形式化能力正在为数学领域构建共享的基础设施。他认为，随着这种底层形式化基础的不断完善，未来数学研究将发生范式转变：数学会像编程语言中的包管理器（如 pip）一样模块化，而定理的证明过程将演变为对不同模块的“导入依赖链（import chains）”。这种结构化的数学基础设施不仅服务于数学本身，未来还将对硬件设计、操作系统、数据库、GPU 内核及编译器等底层计算系统的开发产生深远影响。