Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs
For researchers in formal verification and combinatorics, this neuro-symbolic framework significantly improves automated theorem proving for a class of identities that are challenging for pure LLM-based provers.
WZ-LLM combines the Wilf-Zeilberger method with LLMs to automate formal proofs of combinatorial identities in Lean 4, achieving 34% proof success on LCI-Test, outperforming DeepSeek-V3 and Goedel-Prover-V2.
Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Symbolic methods such as the Wilf-Zeilberger (WZ) method can achieve a mechanized proof of combinatorial identities by constructing special auxiliary functions and demonstrating that they satisfy specific recurrence relations. We propose WZ-LLM, a neuro-symbolic framework that turns WZ proof plans into executable proof sketches in Lean 4 and uses an LLM-based prover to discharge the resulting machine-checkable subgoals. We also train a dedicated WZ-Prover via a Lean-kernel-verified bootstrapping loop with expert-verified iteration, followed by DAPO-based refinement. Experiments show that WZ-LLM achieves a 34% proof success rate on LCI-Test (100 classic combinatorial identities), outperforming strong baselines such as DeepSeek-V3 and Goedel-Prover-V2, and delivering consistent gains on CombiBench and PutnamBench-Comb. These results indicate that our framework provides two complementary strengths: improved direct proving for identities beyond the scope of WZ, and substantially higher end-to-end success when WZ sketches guide a specialized prover.