腾讯会议: 333-715-351 密码: 1122

数学形式化是使用机器基于类型论来严格检查数学证明的方法。与依赖于人类直觉的传统数学证明方法不同，数学形式化要求每一步都经过严格的论证，确保没有任何逻辑上的漏洞或错误。这种方法具有多种优点：提供了对证明正确性的高度信心；已证明的定理和引理可以在其他证明中重复使用，从而鼓励模块化的思考方式；可以自动化证明的某些步骤；由于每一步都明确定义，更容易看出哪里做了特定的假设或采用了哪种逻辑推理。本报告简要介绍数学形式化基础知识，以及在数学优化形式化方面的一些进展。