Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem

• URL: http://arxiv.org/abs/2605.20120v1
• Date: Tue, 19 May 2026 17:08:58 GMT
• Title: Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
• Abstract summary: This paper reports a Lean 4 formalization case study of an Aristotle API proof attempt for the problem, originally posed as IMO 2009 Problem 6.<n>The generated artifact states a generalized Lean version of the theorem, contains four verified helper lemmas for local components of a maximality and adjacent-swap exchange strategy.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: AI-assisted theorem proving can now generate substantial Lean developments for olympiad-level mathematics, but the evidential status of such developments depends on which declarations are actually verified. This paper reports a Lean 4 formalization case study of an Aristotle API proof attempt for the Grasshopper problem, originally posed as IMO 2009 Problem 6. The generated artifact states a generalized Lean version of the theorem, contains four verified helper lemmas for local components of a maximality and adjacent-swap exchange strategy, and leaves the main theorem grasshopper closed directly by one unresolved sorry. The verified components establish that the final partial sum equals the total sum, that an adjacent transposition can affect only the relevant intermediate partial sum, that the changed partial sum has the expected form, and that maximality at a position admitting an adjacent successor swap forces a corresponding forbidden-set membership fact. The Aristotle output summary identifies the intended remaining mathematical step as the global counting step needed to show that these membership facts produce at least n distinct forbidden values, contradicting the cardinality assumption |M| < n; the Lean source itself does not reduce the main theorem to a separately encoded counting lemma. This case study gives an inspectable example of a central limitation in AI-assisted formalization, namely that local proof search can succeed while the global combinatorial bookkeeping required for a theorem remains unresolved. The paper contributes a reproducible Lean artifact and a precise analysis of its verified and unverified proof content.

Related papers

• Autoformalizing Argumentative Material Inferences [26.35292656634472]
  We develop an autoformalization for argumentative material inference as guard completion.<n>GUARD yields significant improvements in verified-faithful.<n>We show that the symbolic soft critique and the explicit assumption layer account for most of these gains.
  arXiv  Detail & Related papers  (2026-09-15T11:05:26Z)
• ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
  We introduce ComBench, an Olympiad-level benchmark for diagnosing and the reasoning capabilities of large language models.<n>ComBench contains 100 human-annotated competition-level problems organized around two complementary settings.<n>Experiments show that the strongest model reaches 65.4% overall Avg. and 75.3% overall Best@4.
  arXiv  Detail & Related papers  (2026-06-09T06:50:15Z)
• TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics [6.168228844241134]
  We introduce TheoremBench, a Lean4 benchmark designed to evaluate theorem provers beyond contest settings.<n>The benchmark is built from nearly one hundred classical theorems and is released in two complementary forms.<n>Our experiments show that explicit premises substantially improve performance for Lean4-capable prover models.
  arXiv  Detail & Related papers  (2026-06-08T12:57:18Z)
• Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory [17.20738506776148]
  Asymptotic statistical theory is a challenging domain for AI-assisted formalization.<n>We propose a hypothesis-disciplined Lean 4 formalization pipeline built from multiple agents.<n>The resulting Lean development is axiom-clean and source-faithful.
  arXiv  Detail & Related papers  (2026-06-03T20:03:38Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• Structured Abductive-Deductive-Inductive Reasoning for LLMs via Algebraic Invariants [0.0]
  Large language models exhibit systematic limitations in structured logical reasoning.<n>We present a symbolic scaffold that operationalizes Peirce's tripartite inference as an explicit protocol for LLM-assisted reasoning.
  arXiv  Detail & Related papers  (2026-04-17T05:59:16Z)
• Exact Structural Abstraction and Tractability Limits [0.0]
  Exact correctness depends only on the induced classes $s sim_R simation' iff mathrmAdm_R(s)$.<n>Decision, search, approximation, statistical, randomized horizon, and distributional guarantees all reduce to this same quotient-recovery problem.
  arXiv  Detail & Related papers  (2026-04-08T17:59:47Z)
• PBLean: Pseudo-Boolean Proof Certificates for Lean 4 [27.126691338850254]
  We present PBLean, a method for importing VeriPB pseudo-Boolean (PB) proof certificates into Lean 4.<n>Key to our approach is reflection: a Boolean checker function whose soundness is fully proved in Lean and executed as compiled native code.<n>Our checker supports all VeriPB kernel rules, including cutting-planes and proof-by-contradiction subproofs.
  arXiv  Detail & Related papers  (2026-02-09T14:13:30Z)
• FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory [44.64175433092553]
  Large language models (LLMs) have recently demonstrated remarkable progress in formal theorem proving.<n>Yet their ability to serve as practical assistants for mathematicians, filling in missing steps within complex proofs, remains underexplored.<n>We introduce FormalML, a Lean 4 benchmark built from foundational theories of machine learning.
  arXiv  Detail & Related papers  (2025-09-26T14:40:14Z)
• CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
  We propose that guiding models to perform a systematic and comprehensive reasoning process allows models to execute much finer-grained and accurate entailment decisions.<n>We define a 3-step reasoning process, consisting of (i) claim decomposition, (ii) sub-claim attribution and entailment classification, and (iii) aggregated classification, showing that such guided reasoning indeed yields improved hallucination detection.
  arXiv  Detail & Related papers  (2025-06-05T17:02:52Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation.<n>For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it.<n>As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)
• Proving Theorems Recursively [80.42431358105482]
  We propose POETRY, which proves theorems in a level-by-level manner. Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level. We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
  arXiv  Detail & Related papers  (2024-05-23T10:35:08Z)

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.