Open Geometry Prover Community Project

• URL: http://arxiv.org/abs/2201.01375v1
• Date: Mon, 3 Jan 2022 09:27:23 GMT
• Title: Open Geometry Prover Community Project
• Authors: Nuno Baeta (University of Coimbra, Portugal), Pedro Quaresma (CISUC, Department of Mathematics, University of Coimbra, Portugal)
• Abstract summary: The Open Geometry Prover Community Project aims at the integration of the different efforts for the development of geometry automated theorem provers, under a common "umbrella" This article describes the necessary steps to such integration and the current implementation of some of those steps.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Mathematical proof is undoubtedly the cornerstone of mathematics. The emergence, in the last years, of computing and reasoning tools, in particular automated geometry theorem provers, has enriched our experience with mathematics immensely. To avoid disparate efforts,the Open Geometry Prover Community Project aims at the integration of the different efforts for the development of geometry automated theorem provers, under a common "umbrella". In this article the necessary steps to such integration are specified and the current implementation of some of those steps is described.

Related papers

• MathBench: Evaluating the Theory and Application Proficiency of LLMs with a Hierarchical Mathematics Benchmark [82.64129627675123]
  MathBench is a new benchmark that rigorously assesses the mathematical capabilities of large language models. MathBench spans a wide range of mathematical disciplines, offering a detailed evaluation of both theoretical understanding and practical problem-solving skills.
  arXiv  Detail & Related papers  (2024-05-20T17:52:29Z)
• Abstraction boundaries and spec driven development in pure mathematics [0.0]
  In this article we discuss how abstraction boundaries can help tame complexity in mathematical research. We argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas.
  arXiv  Detail & Related papers  (2023-09-26T11:59:32Z)
• A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools [0.0]
  The introduction of automated deduction systems in secondary schools face several bottlenecks. The dissonance between the outcomes of the geometry automated theorem provers and the normal practice of conjecturing and proving in schools is a major barrier to a wider use of such tools in an educational environment. A lesson plan is presented, its goal is the introduction of formal demonstration of proving geometric theorems, trying to motivate students to that goal.
  arXiv  Detail & Related papers  (2023-03-10T11:36:10Z)
• UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression [127.68780714438103]
  Two main geometry problems: calculation and proving, are usually treated as two specific tasks. We construct a large-scale Unified Geometry problem benchmark, UniGeo, which contains 4,998 calculation problems and 9,543 proving problems. We also present a unified multi-task Geometric Transformer framework, Geoformer, to tackle calculation and proving problems simultaneously.
  arXiv  Detail & Related papers  (2022-12-06T04:37:51Z)
• Machine Learning Algebraic Geometry for Physics [0.0]
  This chapter is a contribution to the book Machine learning and Algebraic Geometry, edited by A. Kasprzyk and A. Kasprzyk et al.
  arXiv  Detail & Related papers  (2022-04-21T18:00:03Z)
• Learning with symmetric positive definite matrices via generalized Bures-Wasserstein geometry [40.23168342389821]
  We propose a novel generalization of the Bures-Wasserstein geometry, which we call the GBW geometry. We provide a rigorous treatment to study various differential geometric notions on the proposed novel generalized geometry. We also present experiments that illustrate the efficacy of the proposed GBW geometry over the BW geometry.
  arXiv  Detail & Related papers  (2021-10-20T10:03:06Z)
• Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning [123.06420835072225]
  We construct a new large-scale benchmark, Geometry3K, consisting of 3,002 geometry problems with dense annotation in formal language. We propose a novel geometry solving approach with formal language and symbolic reasoning, called Interpretable Geometry Problem solver (Inter-GPS) Inter-GPS incorporates theorem knowledge as conditional rules and performs symbolic reasoning step by step.
  arXiv  Detail & Related papers  (2021-05-10T07:46:55Z)
• A Unifying and Canonical Description of Measure-Preserving Diffusions [60.59592461429012]
  A complete recipe of measure-preserving diffusions in Euclidean space was recently derived unifying several MCMC algorithms into a single framework. We develop a geometric theory that improves and generalises this construction to any manifold.
  arXiv  Detail & Related papers  (2021-05-06T17:36:55Z)
• Bayesian Quadrature on Riemannian Data Manifolds [79.71142807798284]
  A principled way to model nonlinear geometric structure inherent in data is provided. However, these operations are typically computationally demanding. In particular, we focus on Bayesian quadrature (BQ) to numerically compute integrals over normal laws. We show that by leveraging both prior knowledge and an active exploration scheme, BQ significantly reduces the number of required evaluations.
  arXiv  Detail & Related papers  (2021-02-12T17:38:04Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)
• Towards Automated Discovery of Geometrical Theorems in GeoGebra [0.0]
  We describe a prototype of a new experimental GeoGebra command and tool Discover that analyzes geometric figures for salient patterns, properties, and theorems. The paper focuses on the mathematical background of the implementation, as well as methods to avoid explosion when storing the interesting properties of a geometric figure.
  arXiv  Detail & Related papers  (2020-07-24T10:59:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.