经典和现代几何的自动推理和符号计算的高级不变量技术

自吴文俊开创数学机械化领域以来，代数方法成为几何推理的重要手段。这种方法遇到的主要困难是符号计算时的中间表达式膨胀。我们建立的高级不变量理论和技术，拥有强大的高层计算手段，克服了基本不变量系统无法克服的许多计算困难。应用它们证明和扩展经典几何和微分几何定理，使得以前数十万项都难以完成的计算，现在只要一两项就能完成，极大地提高了数学机械化方法的效率。.本项目一方面通过继续研究经典几何和经典不变量理论中的若干公开问题，继续发展高级不变量理论，并利用它在若干公开的经典几何和经典不变量问题上取得进展甚至彻底解决，另一方面在符号维数的黎曼几何符号计算和流形的同调、上同调计算等现代几何的研究方面发展机械化算法，将机械化数学向核心几何学进一步发展，在老一辈数学家一直看好的方向上取得突破。