Cover Image

LeanGeo: Formalizing Competitional Geometry problems in Lean

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Song, Chendong, Wang, Zihan, Pu, Frederick, Wang, Haiming, Lin, Xiaohan, Liu, Junqi, Li, Jia, Liu, Zhengying
Format:	Preprint
Published:	2025
Subjects:	Artificial Intelligence
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
by: Liu, Junqi, et al.
Published: (2026)

FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
by: Lin, Xiaohan, et al.
Published: (2024)

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
by: Santos, Marco Dos, et al.
Published: (2025)

Formally Solving Answer-Construction Problems in Lean
by: Sun, Jialiang, et al.
Published: (2025)

LeanAgent: Lifelong Learning for Formal Theorem Proving
by: Kumarappan, Adarsh, et al.
Published: (2024)

Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4
by: Li, Yuxin, et al.
Published: (2025)

Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
by: Wang, Haiming, et al.
Published: (2025)

FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4
by: Yao, Jiarui, et al.
Published: (2025)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
by: Song, Peiyang, et al.
Published: (2024)

CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics
by: Liu, Junqi, et al.
Published: (2025)

MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
by: Wang, Ruida, et al.
Published: (2025)

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
by: Ospanov, Azim, et al.
Published: (2025)

LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
by: Xu, Rongge, et al.
Published: (2025)

LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
by: Gao, Guoxiong, et al.
Published: (2026)

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
by: Zuo, Ruobing, et al.
Published: (2026)

Formalizing Gröbner Basis Theory in Lean
by: Guo, Junyu, et al.
Published: (2026)

SorryDB: Can AI Provers Complete Real-World Lean Theorems?
by: Letson, Austin, et al.
Published: (2026)

LeanRAG: Knowledge-Graph-Based Generation with Semantic Aggregation and Hierarchical Retrieval
by: Zhang, Yaoze, et al.
Published: (2025)

Lean-STaR: Learning to Interleave Thinking and Proving
by: Lin, Haohan, et al.
Published: (2024)

MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
by: Huang, Yinya, et al.
Published: (2024)

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
by: Zhang, Terry Jingchen, et al.
Published: (2025)

FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean
by: Meadows, Jordan, et al.
Published: (2026)

LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
by: Kripner, Matěj, et al.
Published: (2025)

Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis
by: Zhang, Ke, et al.
Published: (2026)

Herald: A Natural Language Annotated Lean 4 Dataset
by: Gao, Guoxiong, et al.
Published: (2024)

LLMs' Leaning in European Elections
by: Ricciuti, Federico
Published: (2025)

Leaning Time-Varying Instruments for Identifying Causal Effects in Time-Series Data
by: Cheng, Debo, et al.
Published: (2024)

Distilling LLM Feedback for Lean Theorem Proving
by: Narozniak, Gaetan, et al.
Published: (2026)

A Formal Proof of the Irrationality of $ζ(3)$ in Lean 4
by: Liu, Junqi, et al.
Published: (2025)

Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
by: Yanahama, Banri, et al.
Published: (2026)

Beyond Partisan Leaning: A Comparative Analysis of Political Bias in Large Language Models
by: Peng, Tai-Quan, et al.
Published: (2024)

Political Leaning and Politicalness Classification of Texts
by: Volf, Matous, et al.
Published: (2025)

TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
by: Wang, Ruida, et al.
Published: (2024)

CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
by: Long, Wentao, et al.
Published: (2026)

ATG: Benchmarking Automated Theorem Generation for Generative Language Models
by: Lin, Xiaohan, et al.
Published: (2024)

LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
by: Onda, Naoto, et al.
Published: (2025)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
by: Shen, Ziju, et al.
Published: (2025)

Premise Selection for a Lean Hammer
by: Zhu, Thomas, et al.
Published: (2025)

LLMs Lean on Priors, Not Programming Language Semantics
by: Thimmaiah, Aditya, et al.
Published: (2025)

Lyra: Orchestrating Dual Correction in Automated Theorem Proving
by: Zheng, Chuanyang, et al.
Published: (2023)