基于约束求解的合成几何陈述和证明的自动补全方法

Jan, 2024

基于约束求解的合成几何陈述和证明的自动补全方法

Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving

Salwa Tabet Gonzalez, Predrag Janičić, Julien Narboux

TL;DR通过使用合一逻辑和约束求解，我们提出了一个框架，用于补充不完整的猜想和证明。该框架可以将具有缺失假设和不明确目标的猜想转化为正确的定理，并帮助完成草图式证明以使其适于人类阅读和机器检查。

Abstract

conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a

conjecturing theorem proving framework incomplete conjectures incomplete proofs

发现论文，激发创造

基于规则的定理证明器：中学证明入门

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

Mar, 2023

智能辅导系统中几何问题的自动合成

该论文介绍了一个名为 GeoTutor 的智能辅导系统，它能自动合成证明问题及其解决方案，以及针对学生在欧几里得几何方面的缺陷提供个性化练习问题。

Oct, 2015

开放几何证明社区项目

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

Jan, 2022

几何中自动定理生成 / 发现的方法和度量考虑

为了发现并判断几何定理的有趣性，本文针对自动发现几何定理和其性质的不同方法和度量进行讨论，并引入了一个不可判定性结果来证明判断定理生成程序是否能产生有趣定理是一个非确定性任务。此外，还强调了需要通过专家调查和相关度量和方法的研究明确定理生成程序和有趣几何定理之间的关系。

Jan, 2024

中学自动推理入门：四个几何问题

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

Feb, 2022

基于自动正式化的数学和代码正确性研究：基础证明实验

本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。

Jan, 2023

自动形式化欧几里德几何

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

May, 2024

迈向自动可读的直尺和圆规构造证明

本论文展示了我们的三角形构造求解器 ArgoTriCS 如何与一阶逻辑和连续逻辑的自动定理证明器合作，从而生成既可读性强的合成正确性证明，又具有形式化特性的构造解决方案。这些证明依赖于许多高级引理，我们的目标是从几何的基本公理中形式化证明它们全部。

Jan, 2024

Draft, Sketch, and Prove: 用非正式证明指导形式化定理证明器

本文介绍了一种名为 DSP 的方法，可以将非正式证明映射到正式证明草图并指导自动证明器，使其搜索更容易的子问题。实验证明语言模型能够产生结构良好的正式草图，并将其指导自动证明器，从而提高性能达到 39.3%。

Oct, 2022

利用机器智能生成数学猜想

本文提出了一种利用机器智能在数学数据中找到抽象模式生成数学不等式的猜想的系统方法，以 < f<g 类型的严格不等式为重点研究对象，并将它们与一个向量空间相关联，并在这个称为猜想空间的空间中执行几何渐进式下降算法，生成了有关素数计数函数和非阿贝尔简单群的 Cayley 图直径的新猜想，并突显了该空间中数学发现的重要性和领域专业知识的必要性。

Jun, 2023