几何定理机器证明的代数方法的等价性与完全性

The rapid development and tremendous impact of formal verification of mathematical proofs demand the formal verification of the machine proofs generated by theorem-provers in classical geometry based on algebraic methods. The key of this task lies in the equivalence problem of the algebraization of a geometric proposition together with the geometrization of the result of the corresponding algebraic proof, with the original geometric proposition. When this problem is solved, then for the given geometric proposition, exploring the existence of algebraic proofs of any equivalent algebraic proposition without making any specific algebraization and algebraic proof, or even the existence of coordinate-free algebraic proofs, is the completeness problem of algebraic methods. When the answer is positive, then how to find by construction an appropriate algebraization and the corresponding algebraic proving method, how to develop a software as an assistant of geometric theorem-provers and featured in automatic and intelligent algebraization of the geometric input leading to an algebraic proof with completeness, and how to realize full automation in theorem-provers for classical geometry, are a challenging task faced by the development of mathematics mechanization...In this project, we intend to use computer algebra, real algebraic geometry, invariant theory, type theory, and so on, to partially solve the equivalence and completeness problems of algebraic methods for geometric theorem proving, and to develop a mathematical software based on Maple and Coq serving as a preliminary geometric theorem-prover assistant.

在当今数学证明的形式化验证蓬勃发展并产生重大影响的形势下，形式化验证几何定理的代数证明势在必行。这一任务的关键在于几何命题的代数化和证明结果的几何化是否具备与原几何命题的等价性。在此问题解决的基础上，在不进行具体的代数化表示和代数证明之前，探讨给定几何命题是否存在等价的代数命题的代数化证明，甚至是无坐标形式的代数证明，这是代数证明的完全性问题。在该问题的答案是肯定的情况下，如何构造性地找到适当的代数化和相应的代数证明方法，从而开发作为几何定理机器证明辅助器的、针对几何命题完全证明的自动代数化输入，实现几何定理代数证明的完全自动化和智能化，从而有助于代数化机器证明实现形式化验证，这是数学机械化发展所面临的一项挑战。..本项目将利用计算机代数、实代数几何、不变量理论、类型论等工具，部分解决几何定理代数证明的等价性和完全性问题，初步完成基于Maple和Coq的几何定理代数化证明的分析辅助软件。

针对代数证明的等价性与完全性问题，本项目从几何定理的代数证明、微积分定理证明的机器验证两个角度进行了探讨。..几何不变量的标准型计算是等价性判定的一个重要问题。在射影几何、黎曼几何不变量标准型的快速计算中，我们提出了新的快速算法，比此前国际上最好的算法速度提高了两个数量级。共形几何代数可以明显改善代数计算的几何可解释性。我们系统发掘共形几何代数的幂零单项式的经典几何解释，发现了许多重要几何构造的单项式表示；在探讨这种几何可解释性的内在代数机制中，获得了共形几何代数的幂零单项式分解的标准型，由此推导出一般线性四元数方程的无基底形式解。..针对微积分数学问题的逻辑推理、符号演算混合证明的机器验证，我们从符号计算角度出发，提出极限、微分、积分等类型的不等式关系判定高效方法，形成若干算法，并编写成Maple软件包，在微积分数学问题的逻辑与符号计算混合证明的验证中进行了测试。结果表明，基于这些方法的验证函数不仅在不等式验证、逻辑推理的符号计算实现等方面比现有Maple系统自带的判定函数强大很多，而且在证明漏洞的智能补充、ε-δ格式的智能生成等方面独树一帜。..相关成果发表于有基金标注的研究论文12篇，包括符号计算国际顶级会议ISSAC 2017、2018等，被国际同行认为“比已有最好方法有显著提高”，是“重要贡献”。