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

Salwa Tabet Gonzalez, Predrag Janičić, Julien Narboux
1/22/2024
cs.AIcs.LO

No official code found. Best implementation: janicicpredrag/Larus (10 stars, GPL-3.0, last commit 2026-04-28).

Abstract

Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions and with an under-specified goal into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof. Our approach is focused on synthetic geometry, and uses coherent logic and constraint solving. The proposed approach is uniform for all three kinds of tasks, flexible and, to our knowledge, unique such approach.

View on arXivView PDF

Code Implementations(1)

janicicpredrag/LarusCommunity100%
GPL-3.0

Larus is a theorem prover for coherent logic that uses SAT/SMT provers to construct proofs. Larus can generate natural language proofs (in LaTeX) and verifiable Coq proofs.

103C, C++Dec 29, 20195 months agoGPL-3.0

Similar Papers

Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry

82% match2024

LeanGeo: Formalizing Competitional Geometry problems in Lean

79% match1 repo432025

LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving

78% match2025

Learning Formal Mathematics From Intrinsic Motivation

78% match1 repo362024

FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving

77% match1 repo182023

An AI-Assisted Formalization of the Poincaré Conjecture

77% match2026

Cite this paper

@article{gonzalez2024automated,
  title  = {Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving},
  author = {Salwa Tabet Gonzalez and Predrag Janičić and Julien Narboux},
  year   = {2024},
  eprint = {2401.11898},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2401.11898v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2401.11898.svg)](https://codeofpaper.com/paper/2401.11898)

Discussion