Image de couverture de livre

Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Xiong, Beibei, Lv, Hangyu, Liu, Junqi, Wang, Yisen, Chen, Shaoshi, Wang, Jianlin, Yang, Zhengfeng, Zhi, Lihong
Format:	Preprint
Publié:	2026
Sujets:	Machine Learning
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
par: Xiong, Beibei, et autres
Publié: (2025)

How to generate all possible rational Wilf-Zeilberger forms?
par: Chen, Shaoshi, et autres
Publié: (2024)

Symbolic Integration of Differential Forms: From Abel to Zeilberger
par: Chen, Shaoshi, et autres
Publié: (2026)

A Formal Proof of the Irrationality of $ζ(3)$ in Lean 4
par: Liu, Junqi, et autres
Publié: (2025)

Wilf-Zeilberger seeds and non-trivial hypergeometric identities
par: Au, Kam Cheong
Publié: (2023)

Discovering hypergeometric series with harmonic numbers via Wilf-Zeilberger seeds
par: Au, Kam Cheong
Publié: (2026)

$q$-analogues of Wilf-Zeilberger seeds and Ramanujan $1/π^k$-formulas
par: Au, Kam Cheong
Publié: (2024)

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
par: Zuo, Ruobing, et autres
Publié: (2026)

CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics
par: Liu, Junqi, et autres
Publié: (2025)

Formalizing Gröbner Basis Theory in Lean
par: Guo, Junyu, et autres
Publié: (2026)

Automated Proof of Polynomial Inequalities via Reinforcement Learning
par: Liu, Banglong, et autres
Publié: (2025)

Automated Tactics for Polynomial Reasoning in Lean 4
par: Shen, Hao, et autres
Publié: (2026)

Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
par: Qiu, Ruichen, et autres
Publié: (2026)

On the Summability Problem of Multivariate Rational Functions in the Mixed Case
par: Chen, Shaoshi, et autres
Publié: (2026)

Proof of a conjecture on the shape-Wilf-equivalence for partially ordered patterns
par: Wang, Lintong, et autres
Publié: (2025)

CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization
par: Shi, Shuming, et autres
Publié: (2025)

Generalization and Probabilistic Proofs of Some Combinatorial Identities
par: Vellaisamy, Palaniappan, et autres
Publié: (2026)

Guidance Design for Escape Flight Vehicle Using Evolution Strategy Enhanced Deep Reinforcement Learning
par: Hu, Xiao, et autres
Publié: (2024)

Non-minimality of minimal telescopers explained by residues
par: Chen, Shaoshi, et autres
Publié: (2025)

Combinatorial Proofs of Ismail's Identities on Al-Salam--Chirara Polynomials
par: Uncu, Ali K.
Publié: (2026)

Formalizing Wu-Ritt Method in Lean 4
par: Xiao, Yuxuan, et autres
Publié: (2026)

Automated Formalization via Conceptual Retrieval-Augmented LLMs
par: Lu, Wangyue, et autres
Publié: (2025)

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
par: Liu, Junqi, et autres
Publié: (2026)

An Algorithm for Diagonalizing Matrices of Formal Power Series
par: Dai, Zihao, et autres
Publié: (2026)

Bijections for generalized Wilf equivalences
par: Ferreri, Melanie
Publié: (2024)

Combinatorial Proofs for Overpartitions and Two-Colored Partitions II
par: Chen, Dandan, et autres
Publié: (2025)

A Unified Proof of Three Combinatorial Identities Related to the Stirling Numbers of the Second Kind
par: He, Chun-Ying, et autres
Publié: (2025)

On Formality and Combinatorial Formality for hyperplane arrangements
par: Möller, Tilman, et autres
Publié: (2022)

Translating Informal Proofs into Formal Proofs Using a Chain of States
par: Wang, Ziyu, et autres
Publié: (2025)

Palindrome Partitions and the Calkin-Wilf Tree
par: Hemmer, David J., et autres
Publié: (2024)

Power series expansion of Wilf function
par: Qi, Feng
Publié: (2021)

Combinatorial Optimization with Automated Graph Neural Networks
par: Liu, Yang, et autres
Publié: (2024)

Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically
par: Dong, Kefan, et autres
Publié: (2024)

Towards Automated Formal Verification of Backend Systems with LLMs
par: Xu, Kangping, et autres
Publié: (2025)

Meeting a Challenge raised by Ekhad and Zeilberger related to Stern's Triangle
par: Tang, Jinlong, et autres
Publié: (2025)

Advancing Speech Summarization in Multi-modal LLMs with Reinforcement Learning
par: Ling, Shaoshi, et autres
Publié: (2025)

Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs
par: Ma, Zhi, et autres
Publié: (2025)

Long-Short Alignment for Effective Long-Context Modeling in LLMs
par: Du, Tianqi, et autres
Publié: (2025)

APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
par: Xin, Huajian, et autres
Publié: (2025)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
par: Cao, Jialun, et autres
Publié: (2025)