Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Similar Items
A Modular First Formalisation of Combinatorial Design Theory
by: Edmonds, Chelsea, et al.
Published: (2021)
by: Edmonds, Chelsea, et al.
Published: (2021)
Formalising New Mathematics in Isabelle: Diagonal Ramsey
by: Paulson, Lawrence C
Published: (2025)
by: Paulson, Lawrence C
Published: (2025)
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
by: Edmonds, Chelsea, et al.
Published: (2023)
by: Edmonds, Chelsea, et al.
Published: (2023)
Formalizing Pick's Theorem in Isabelle/HOL
by: Binder, Sage, et al.
Published: (2024)
by: Binder, Sage, et al.
Published: (2024)
Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
by: Wiesnet, Franziskus
Published: (2025)
by: Wiesnet, Franziskus
Published: (2025)
The continuous functional calculus in Lean
by: Dedecker, Anatole, et al.
Published: (2025)
by: Dedecker, Anatole, et al.
Published: (2025)
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
by: Edmonds, Chelsea, et al.
Published: (2022)
by: Edmonds, Chelsea, et al.
Published: (2022)
Anatomy of a Formal Proof
by: Avigad, Jeremy, et al.
Published: (2024)
by: Avigad, Jeremy, et al.
Published: (2024)
Measurability in the Fundamental Theorem of Statistical Learning
by: Krapp, Lothar Sebastian, et al.
Published: (2024)
by: Krapp, Lothar Sebastian, et al.
Published: (2024)
A Cut-Free Sequent Calculus for the Analysis of Finite-Trace Properties in Concurrent Systems
by: Fusco, Ludovico, et al.
Published: (2025)
by: Fusco, Ludovico, et al.
Published: (2025)
An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility
by: Farmer, William M.
Published: (2026)
by: Farmer, William M.
Published: (2026)
Universal truth of operator statements via ideal membership
by: Hofstadler, Clemens, et al.
Published: (2022)
by: Hofstadler, Clemens, et al.
Published: (2022)
A formalization of Borel determinacy in Lean
by: Manthe, Sven
Published: (2025)
by: Manthe, Sven
Published: (2025)
A new decision method for Intuitionistic Logic by 3-valued non-deterministic truth-tables (pre-print version)
by: Leme, Renato, et al.
Published: (2023)
by: Leme, Renato, et al.
Published: (2023)
A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
by: Ramos, Arthur F., et al.
Published: (2026)
by: Ramos, Arthur F., et al.
Published: (2026)
Unboring ideals
by: Kwela, Adam
Published: (2021)
by: Kwela, Adam
Published: (2021)
PatternBoost: Constructions in Mathematics with a Little Help from AI
by: Charton, François, et al.
Published: (2024)
by: Charton, François, et al.
Published: (2024)
Remarks on Halin's end-degree Conjecture
by: Fernandes, Gabriel
Published: (2024)
by: Fernandes, Gabriel
Published: (2024)
Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
by: Wang, Zili, et al.
Published: (2025)
by: Wang, Zili, et al.
Published: (2025)
Formalizing MLTL Formula Progression in Isabelle/HOL
by: Kosaian, Katherine, et al.
Published: (2024)
by: Kosaian, Katherine, et al.
Published: (2024)
Remote Verification System for Mizar Integrated with Emwiki
by: Kai, Toshiki, et al.
Published: (2024)
by: Kai, Toshiki, et al.
Published: (2024)
Proof-Theoretic Relations between Higman's and Kruskal's theorem, and Independence Results for Tree-like Structures
by: Buriola, Gabriele, et al.
Published: (2025)
by: Buriola, Gabriele, et al.
Published: (2025)
The uniform Kruskal theorem over RCA$_0$
by: Uftring, Patrick
Published: (2025)
by: Uftring, Patrick
Published: (2025)
The Ordering Principle and Dependent Choice
by: Holy, Peter, et al.
Published: (2025)
by: Holy, Peter, et al.
Published: (2025)
The Ordering Principle and Higher Dependent Choice
by: Holy, Peter, et al.
Published: (2025)
by: Holy, Peter, et al.
Published: (2025)
Lebesgue measure zero modulo ideals on the natural numbers
by: Gavalová, Viera, et al.
Published: (2022)
by: Gavalová, Viera, et al.
Published: (2022)
Aristotle's Second-Order Logic and Natural Deduction
by: Protin, Clarence
Published: (2023)
by: Protin, Clarence
Published: (2023)
Extension realizing affine datum: low-dimensional cohomology
by: Wires, Alexander
Published: (2023)
by: Wires, Alexander
Published: (2023)
A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem
by: Brossard, Jonathan
Published: (2026)
by: Brossard, Jonathan
Published: (2026)
A Higher-Order Vampire (Short Paper)
by: Bhayat, Ahmed, et al.
Published: (2024)
by: Bhayat, Ahmed, et al.
Published: (2024)
Forcing Diamond and Applications to Iterability
by: Mildenberger, Heike, et al.
Published: (2025)
by: Mildenberger, Heike, et al.
Published: (2025)
Introducing a nontrivial square_omega
by: Dolinar, Gregor K., et al.
Published: (2010)
by: Dolinar, Gregor K., et al.
Published: (2010)
Sealed Kurepa Trees
by: Giron, Itamar, et al.
Published: (2023)
by: Giron, Itamar, et al.
Published: (2023)
Some combinatorial properties of semiselective ideals
by: Cano, Julián C., et al.
Published: (2023)
by: Cano, Julián C., et al.
Published: (2023)
Artifical intelligence and inherent mathematical difficulty
by: Dean, Walter, et al.
Published: (2024)
by: Dean, Walter, et al.
Published: (2024)
Evolving Local Corrections for Global Constructions in Combinatorics
by: Bérczi, Gergely
Published: (2026)
by: Bérczi, Gergely
Published: (2026)