Can a Lightweight Automated AI Pipeline Solve Research-Level Mathematical Problems?
Lve Meng, Weilong Zhao, Yanzhi Zhang, Haoxiang Guan, Jiyan He
cs.AI
Feb 14, 2026 · v2
math.AC math.CO math.CT
TL;DR
After the LLM pipeline produced a proof of First Proof Problem 4, the authors attempted a Lean 4 formalization exceeding 5,000 lines.
Abstract
Large language models (LLMs) have recently achieved remarkable success in generating rigorous mathematical proofs, with "AI for Math" emerging as a vibrant field of research (Ju et al., 2026). While these models have mastered competition-level benchmarks like the International Mathematical Olympiad (Huang et al., 2025; Duan et al., 2025) and show promise in research applications through auto-formalization (Wang et al., 2025), their deployment via lightweight, natural-language pipelines for research problems remains underexplored. In this work, we demonstrate that next-generation models (e.g., Gemini 3 Pro, GPT-5.2 Pro), when integrated into a streamlined automated pipeline optimized for citation-based verification, can solve sophisticated research-grade problems. We evaluate our pipeline on two novel datasets: (1) the ICCM (2025) problem sets (comparable to the S.-T. Yau College Student Mathematics Contest) proposed by leading mathematicians (Shanghai Math Challenge, 2026), and (2) the "First Proof" problem set (Abouzaid et al., 2026), consisting of previously unpublished research questions. Our pipeline generated candidate proofs for all problems in the first two ICCM sets and the "First Proof" set. The solutions for the first two ICCM sets and Problem 4 of the "First Proof" set have been fully verified by our team. All generated proofs have been submitted to the official organization, and our generated results are publicly available at
https://github.com/ml1301215/question_sets-test_results. We have open-sourced the code and developed a user-friendly UI for this workflow, accessible at
https://github.com/ml1301215/research-math-assistant.
Problem
It is unclear whether lightweight, natural-language LLM pipelines can solve research-level mathematics problems rather than just competition problems. Formal auto-formalization guarantees correctness but is a high barrier for mathematicians.
Approach
The authors adapt an existing IMO-level automated pipeline with domain-specific prompts for graduate-level reasoning. They add citation-augmented verification, which requires the model to give bibliographic references for non-trivial claims. The pipeline, using models such as Gemini 3 Pro and GPT-5.2 Pro, is evaluated on the ICCM problem sets and the First Proof research problem set. The proof of First Proof Problem 4, an inequality for finite free additive convolution, was then partially formalized in Lean 4.
Results
The pipeline generated candidate proofs for all problems in the first two ICCM sets and the First Proof set. The team verified the solutions to the first two ICCM sets and to First Proof Problem 4. The attempted Lean 4 formalization of the Problem 4 proof exceeded 5,000 lines. Verification, not generation, is identified as the main bottleneck.
