Open Geometry Prover Community Project
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed of competition problems, hillclimbing t…
DeepAlgebra - an outline of a program
We outline a program in the area of formalization of mathematics to automate theorem proving in algebra and algebraic geometry. We propose a construction of a dictionary between automated theorem provers and (La)TeX expl…
Automated Theorem ProvingHUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
We introduce HunyuanProver, an language model finetuned from the Hunyuan 7B for interactive automatic theorem proving with LEAN4. To alleviate the data sparsity issue, we design a scalable framework to iterative synthesi…
Automated Theorem ProvingLanguage ModelingLanguage ModellingProject proposal: A modular reinforcement learning based automated theorem prover
We propose to build a reinforcement learning prover of independent components: a deductive system (an environment), the proof state representation (how an agent sees the environment), and an agent training algorithm. To …
OpenAI Gymreinforcement-learningReinforcement LearningReinforcement Learning (RL)+1LeanGeo: Formalizing Competitional Geometry problems in Lean
Geometry problems are a crucial testbed for AI reasoning capabilities. Most existing geometry solving systems cannot express problems within a unified framework, thus are difficult to integrate with other mathematical fi…