基于Lean的数学形式化简介

来源：计算数学杂志2025年第2期北京时间：

作者：李晨毅, 文再文

单位：北京大学北京国际数学研究中心, 北京 100871

摘要：本文粗略地探讨数学形式化的基本原理与应用, 重点介绍形式化语言Lean及其在数学优化中的应用进展. 我们先回顾数学形式化的发展背景, 阐述形式化语言Lean的构建原理及其正确性保障机制, 介绍Lean语言中的定理库Mathlib4的作用. 通过自然语言与形式化证明的对比, 阐述利用形式化验证数学的优势, 强调形式化在数学理论的准确验证中的重要作用. 在数学优化领域, 本文讨论目前数学优化理论的形式化进展, 以二次上界引理等经典定理的形式化实例, 进一步给出形式化数学的特点与优势. 此外, 我们探讨运筹优化中的形式化目标, 以及自动形式化和自动定理证明的可能性, 分析自动化工具在数学形式化过程中的潜力与挑战. 最后总结数学形式化的研究现状, 提出一些推动形式化领域发展的建议, 并探讨形式化在应用数学理论发展中的重要意义.

关键词：形式化,优化,计算数学

基金资助：国家重点研发计划项目(2024YFA1012903)和国家自然科学基金(12331010,12288101)资助.