3 papers
cs.AI2026
Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
Junqi Liu, Zihao Zhou, Zekai Zhu +10
Agentic systems have recently become the dominant paradigm for formal theorem proving, achieving strong performance by coordinating multiple models and tools. However, existing app…
cs.AI2025
CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics
Junqi Liu, Xiaohan Lin, Jonas Bayer +12
Neurosymbolic approaches integrating large language models with formal reasoning have recently achieved human-level performance on mathematics competition problems in algebra, geom…
math.NT2025
A Formal Proof of the Irrationality of in Lean 4
Junqi Liu, Jujian Zhang, Lihong Zhi
We formalize a proof of the irrationality of in Lean 4, using Beukers' method. To support this, we extend the Lean mathematical library (Mathlib) by formalizing shifted Lege…