2 papers
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…