使用计算机和 GeoGebra Discovery 等软件工具，我们解决了 N'aboj 2023 竞赛中的一些几何问题，并通过符号计算分析了输入机器的困难，设定了未来使此类竞赛问题更易解决的目标。

Jan, 2024

本文探讨了在信息和通信技术的帮助下使用自动推理工具解决几何问题的实验，以解决在中学自动推理系统引入中所面临的难题。

Feb, 2022

本文介绍了 ThEdu 系列以及本卷在 STEM 教育中应用定理证明技术的自动演绎和应用于教育软件的方法和工具在教育方面的应用。

Mar, 2023

介绍了在中学引入自动推理系统面临的几个瓶颈，讨论了一个基于推理规则和自动方法的实现并使用其进行几何猜想的证明，旨在介绍几何定理的形式证明，以激发学生的兴趣。

Mar, 2023

我们通过 GeoGebra Discovery 中的自动推理工具解决了奥地利数学奥林匹克 2023 年的一个问题，并且描述了其中的四种反馈形式：即时的自动解答、根据最新提案进行复杂性评估、找到给定命题的更一般化命题，以及使用 LocusEquation 命令时出现的大量退化情况的分析困难。

Jan, 2024

该研究论文通过探索定理证明技术在 STEM 教育中的软件支持，以实现从中学的直观数学方式到更正式学科的平滑过渡，并促进计算机科学家、数学家和教育者之间的相互理解。

Apr, 2024

本文介绍了一种自动形式化欧几里得几何的神经符号框架，该框架结合了领域知识、SMT 求解器和大型语言模型，这一框架的挑战之一在于通过定理证明器自动填充图形信息以简化模型，实验结果展示了自动形式化几何问题时最新的语言模型的能力和局限性。

May, 2024

本文介绍了一个名为 FGeoDRL 的神经符号系统，用于自动执行类似人类的几何演绎推理。该系统通过强化学习建立策略网络进行定理选择，并使用蒙特卡洛树搜索进行启发式探索。实验结果表明，在形式化数据集上，FGeoDRL 实现了 86.40％的几何问题求解成功率。

Feb, 2024

在过去十年的工作中，我们构建了一个完整且兼容的平面几何形式系统，该系统在 IMO 级别的平面几何挑战和可读的 AI 自动推理之间建立了重要的桥梁。通过这个形式系统，我们成功地将现代 AI 模型与形式系统无缝整合。在这个形式框架内，AI 能够像处理其他自然语言一样，为 IMO 级别的平面几何问题提供演绎推理解决方案，并且这些证明是可读、可追溯和可验证的。我们提出了几何形式化理论（GFT）来指导几何形式系统的发展。根据 GFT，我们构建了 FormalGeo，它包含 88 个几何谓词和 196 个定理，可以表示、验证和解决 IMO 级别的几何问题。我们还使用 Python 开发了 FGPS（形式几何问题解决器），它既可作为交互式助手验证问题解决过程，又可作为自动化问题解决器利用前向搜索、后向搜索和 AI 辅助搜索等多种方法。我们标注了 FormalGeo7k 数据集，其中包含 6,981 个几何问题的完整形式语言注释（通过数据增强扩展为 186,832 个问题）。对形式系统的实施和对 FormalGeo7k 的实验验证了 GFT 的正确性和实用性。后向深度优先搜索方法只有 2.42% 的问题解决失败率，而我们可以结合深度学习技术实现更低的失败率。FGPS 和 FormalGeo7k 数据集的源代码可在此 https URL 获取。

Oct, 2023

本文描述了 Open Geometry Prover Community Project 的目标和实施步骤，旨在将不同自动几何定理证明工具的开发整合到一个共同的 “伞下”，以丰富人们的数学体验。

Jan, 2022