5 papers
MechMath Agent Team: LLM Driven Agents for Mathematical Research
Yichuan Cao, Ruichen Qiu, Junqi Liu +5
AI reasoning has become a central focus in contemporary artificial intelligence, largely driven by the success of large language models. However, mathematical research, which is ch…
Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number
Yichuan Cao, Dakai Guo, Ruichen Qiu +2
In this paper, it is proved that any nonnegative integer can be written in the following form This settles the…
A Greatest Common Divisor Criterion of Certain Binomial Coefficients
Dakai Guo, Ruichen Qiu, Yichuan Cao +2
The binomial greatest common divisor (gcd) criterion recorded as OEIS A080170 is proven. The criterion also appears as conjecture (17) in Ralf Stephan's list of OEIS conjectures. F…
A Finite Certificate for the Positive Vasc Inequality
Dakai Guo, Ruichen Qiu, Yichuan Cao +1
We prove the positive-real case of the Vasc cyclic inequality. The proof was obtained with human-guided assistance from the AI agent MechMath Agent Team: the human-readable p…
MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
Ruichen Qiu, Yichuan Cao, Junqi Liu +4
Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems that require c…