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