Cover Image

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Zuo, Ruobing, Zhao, Hanrui, He, Gaolei, Yang, Zhengfeng, Wang, Jianlin
Format:	Preprint
Published:	2026
Subjects:	Artificial Intelligence
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization
by: Shi, Shuming, et al.
Published: (2025)

A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
by: Xiong, Beibei, et al.
Published: (2025)

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

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

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

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

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

Automated Conjecture Resolution with Formal Verification
by: Ju, Haocheng, et al.
Published: (2026)

Neural Sum-of-Squares: Certifying the Nonnegativity of Polynomials with Transformers
by: Pelleriti, Nico, et al.
Published: (2025)

EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty
by: Tian, Yuchen, et al.
Published: (2025)

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
by: Liu, Chengwu, et al.
Published: (2026)

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

Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
by: Li, Zenan, 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)

LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
by: Lai, Junyu, et al.
Published: (2025)

LeanGeo: Formalizing Competitional Geometry problems in Lean
by: Song, Chendong, et al.
Published: (2025)

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

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

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

Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities
by: Zhao, Haoyu, et al.
Published: (2025)

GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving
by: Wang, Ruida, et al.
Published: (2025)

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
by: Dong, Kefan, et al.
Published: (2025)

FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
by: Uluşan, Zeynel A., et al.
Published: (2026)

Steering LLMs for Formal Theorem Proving
by: Kirtania, Shashank, et al.
Published: (2025)

Mathesis: Towards Formal Theorem Proving from Natural Languages
by: Xuejun, Yu, et al.
Published: (2025)

Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
by: Ji, Xingguang, et al.
Published: (2025)

OProver: A Unified Framework for Agentic Formal Theorem Proving
by: Ma, David, et al.
Published: (2026)

MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification
by: Li, Sirui, et al.
Published: (2025)

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

A Minimal Agent for Automated Theorem Proving
by: Requena, Borja, et al.
Published: (2026)

PBLean: Pseudo-Boolean Proof Certificates for Lean 4
by: Szeider, Stefan
Published: (2026)

LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
by: George, Robert Joseph, et al.
Published: (2025)

What are the Right Symmetries for Formal Theorem Proving?
by: Olejniczak, Krzysztof, et al.
Published: (2026)

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
by: Chen, Luoxin, et al.
Published: (2025)

Hypothesis Generation via LLM-Automated Language Bias for ILP
by: Yang, Yang, et al.
Published: (2025)

Sum of Squares Circuits
by: Loconte, Lorenzo, et al.
Published: (2024)

Aristotle: IMO-level Automated Theorem Proving
by: Achim, Tudor, et al.
Published: (2025)

Formal Verification of Neural Certificates Done Dynamically
by: Henzinger, Thomas A., et al.
Published: (2025)

Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
by: Dougherty, Quinn, et al.
Published: (2025)

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
by: Rao, Balaji, et al.
Published: (2025)