几何代数方法的形式化与实现
Formalization and Implementation of Algebraic Methods in Geometry
摘要：
我们描述了我们正在进行的项目的代数方法的形式化几何定理证明（吴的方法和Groebner基地的方法），其实施和整合的教育工具。该项目包括对Isabelle/HOL证明助手中的代数方法进行形式化验证，并开发一个新的、开源的代数方法Java实现。该项目应填补这一领域仍然存在的一些空白（例如，代数方法和综合几何之间缺乏正式的联系，以及缺乏适合于与动态几何工具集成的代数方法的独立实现），并且应该能够在教育中实现定理证明的新应用。
英文摘要：
We describe our ongoing project of formalization of algebraic methods for geometry theorem proving (Wu's method and the Groebner bases method), their implementation and integration in educational tools. The project includes formal verification of the algebraic methods within Isabelle/HOL proof assistant and development of a new, open-source Java implementation of the algebraic methods. The project should fill-in some gaps still existing in this area (e.g., the lack of formal links between algebraic methods and synthetic geometry and the lack of self-contained implementations of algebraic methods suitable for integration with dynamic geometry tools) and should enable new applications of theorem proving in education.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
