Lihong Zhi — accepted AI-conference papers

2026

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

Beibei Xiong, Hangyu Lv, Junqi Liu, Yisen Wang, Shaoshi Chen, Jianlin Wang +2

ICML 2026spotlight

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 con…

Cited by 0 Source ↗Scholar ↗

2026

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, jiawei liu +6

ICML 2026poster

Agentic systems have recently become the dominant paradigm for formal theorem proving, achieving strong performance by coordinating multiple models and tools. However, existing approaches often rely on task-specific pipelines and trained formal provers, limiting their flexibility and reproducibility…

Cited by 0 Source ↗Scholar ↗