3 papers
cs.SC2026
A Proof of the Dittert Conjecture in Dimension 4 via an Exact Constrained Sum-of-Squares Certificate
Jinhui Li, Beibei Xiong, Zhengfeng Yang
The Dittert conjecture states that the Dittert functional on nonnegative matrices whose entries sum to is uniquely maximized by the uniform matrix. We prove the con…
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…
cs.AI2025
A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
Beibei Xiong, Hangyu Lv, Haojia Shan +3
Large language models (LLMs) have significantly advanced formal theorem proving, yet the scarcity of high-quality training data constrains their capabilities in complex mathematica…