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

Beibei Xiong, Hangyu Lv, Junqi Liu +5

Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Sym…