The automated theorem proving community celebrates each new benchmark conquered: miniF2F problems solved, IMO questions answered, Mathlib theorems reproven. These achievements are genuine and impressive. But they share a common limitation: the problems are known to be solvable. Competition problems have solutions that fit on a single page. Textbook exercises have answers in the back. Mathlib theorems have proofs that human mathematicians have already written.

Research-level mathematics is qualitatively different. The problems may not have solutions. The techniques required may not exist yet. The formalization of the problem statement itself may require mathematical insight. The gap between solving known problems and contributing to open research is the gap between a talented student and a working mathematician—and it is enormous.

Poiroux et al.'s RLMEval (presented at EMNLP Findings) confronts this gap directly by evaluating neural theorem provers on research-level mathematics from real published papers. The results provide a sobering calibration of where AI mathematical reasoning actually stands.

The Benchmark Design

RLMEval collects theorems from recent mathematical publications—real results that working mathematicians proved and published. The theorems span multiple mathematical subdisciplines and difficulty levels, from routine lemmas (technical results needed for the main theorems) to the main theorems themselves.

Each theorem is provided in two forms:

• Informal statement: The theorem as written in the paper (natural language with mathematical notation)
• Formal statement: The theorem formalized in Lean (machine-verifiable specification)

What the Results Reveal

The findings are instructive in their specificity:

Routine lemmas: Neural provers handle many routine lemmas—straightforward consequences of definitions, applications of known theorems, algebraic manipulations. These are the mathematical equivalent of "boilerplate code"—necessary but not creative.

Non-trivial intermediate results: Provers struggle with intermediate results that require choosing the right mathematical technique from several possibilities. Unlike competition problems where the technique is often hinted by the problem context, research mathematics requires the prover to autonomously select from a large toolbox.

Main theorems: Current provers rarely succeed on main theorems of published papers. These theorems typically require novel proof strategies that combine techniques in ways not seen in the training data—precisely the capability that defines mathematical research.

Autoformalization: Translating informal mathematical statements to formal specifications is itself a challenging task. Mathematical notation is ambiguous (the same symbol means different things in different contexts), implicit assumptions are common (domain experts share unstated conventions), and formalization choices affect proof difficulty.

The Gap Analysis

RLMEval enables a precise gap analysis between current AI capability and research-level mathematics:

The progression from routine to creative mirrors the human mathematical development trajectory—and current AI systems are roughly at the graduate student level: competent with known techniques, struggling when creativity is required.

Claims and Evidence

Open Questions

What This Means for Your Research

For AI researchers working on mathematical reasoning, RLMEval provides the most honest assessment of current capability. Competition benchmarks are useful for measuring progress but create a misleading impression of proximity to genuine mathematical research capability. The gap is large—and closing it requires advances in creative reasoning that current architectures may not support.

For mathematicians, RLMEval calibrates expectations. AI proof assistants can genuinely help with routine proof obligations—freeing human effort for creative work. But the headline-grabbing results on competition problems should not be extrapolated to research mathematics. The creative core of mathematical research remains distinctly human—for now.

For the mathematical community broadly, RLMEval raises the question of what mathematical research really is. If routine lemmas can be automated and competition problems can be solved, the uniquely human contribution to mathematics is increasingly concentrated in the creative acts of conjecture, strategy selection, and conceptual insight that current AI systems cannot perform.

면책 조항: 이 게시물은 정보 제공 목적의 연구 동향 개요이다. 학술 연구에서 인용하기 전에 특정 발견, 통계 및 주장은 원본 논문과 대조하여 검증해야 한다.

RLMEval: 신경 정리 증명기는 연구 수준의 수학을 다룰 수 있는가?

자동 정리 증명 커뮤니티는 새로운 벤치마크가 정복될 때마다 이를 축하한다: miniF2F 문제 해결, IMO 문제 답변, Mathlib 정리 재증명. 이러한 성과들은 진정하고 인상적이다. 그러나 이들은 공통된 한계를 공유한다: 해당 문제들은 풀 수 있다는 것이 이미 알려져 있다. 경시대회 문제는 한 페이지에 맞는 풀이가 존재한다. 교재 연습문제는 뒤에 답이 있다. Mathlib 정리는 인간 수학자들이 이미 작성한 증명이 있다.

연구 수준의 수학은 질적으로 다르다. 문제에 풀이가 존재하지 않을 수 있다. 필요한 기법이 아직 존재하지 않을 수 있다. 문제 진술 자체의 형식화도 수학적 통찰을 요구할 수 있다. 알려진 문제를 푸는 것과 열린 연구에 기여하는 것 사이의 간극은 재능 있는 학생과 현직 수학자 사이의 간극과 같으며—그 간극은 엄청나다.

Poiroux 외 연구진의 RLMEval(EMNLP Findings 발표)은 실제 출판된 논문에서 가져온 연구 수준의 수학으로 신경 정리 증명기를 평가함으로써 이 간극을 정면으로 다룬다. 그 결과는 AI 수학적 추론이 실제로 어느 수준에 있는지를 냉정하게 보정해 준다.

벤치마크 설계

RLMEval은 최근 수학 출판물로부터 정리를 수집한다—현직 수학자들이 증명하고 발표한 실제 결과들이다. 해당 정리들은 여러 수학 하위 분야와 난이도 수준에 걸쳐 있으며, 일상적인 보조 정리(주요 정리에 필요한 기술적 결과)부터 주요 정리 자체까지 포함된다.

각 정리는 두 가지 형태로 제공된다:

• 비형식적 진술: 논문에 작성된 그대로의 정리 (수학적 표기법을 포함한 자연어)
• 형식적 진술: Lean으로 형식화된 정리 (기계 검증 가능한 명세)

결과가 드러내는 것

발견들은 그 구체성에서 교훈적이다:

일상적인 보조 정리: 신경 증명기는 많은 일상적인 보조 정리를 다룬다—정의의 직접적인 귀결, 알려진 정리의 적용, 대수적 조작. 이것들은 수학적으로 "반복 코드"에 해당한다—필요하지만 창의적이지 않다.

비자명한 중간 결과: 증명기는 여러 가능성 중에서 올바른 수학적 기법을 선택해야 하는 중간 결과에서 어려움을 겪는다. 문제 맥락에서 기법이 암시되는 경우가 많은 경시대회 문제와 달리, 연구 수학에서는 증명기가 방대한 도구상자에서 자율적으로 선택해야 한다.

주요 정리: 현재의 증명기는 출판된 논문의 주요 정리에서 거의 성공하지 못한다. 이러한 정리들은 일반적으로 훈련 데이터에서 볼 수 없는 방식으로 기법들을 결합하는 새로운 증명 전략을 요구한다—이것이 바로 수학 연구를 정의하는 능력이다.

자동 형식화: 비형식적 수학적 진술을 형식적 명세로 번역하는 것 자체가 어려운 과제이다. 수학적 표기법은 모호하고(같은 기호가 다른 맥락에서 다른 것을 의미한다), 암묵적 가정이 일반적이며(분야 전문가들은 명시되지 않은 관례를 공유한다), 형식화 선택이 증명 난이도에 영향을 미친다.

간극 분석

RLMEval은 현재 AI 능력과 연구 수준 수학 사이의 정밀한 간극 분석을 가능하게 한다:

주장과 증거

미해결 질문

일상적인 것에서 창의적인 것으로의 진행은 인간의 수학적 발달 궤적을 반영하며, 현재의 AI 시스템은 대략 대학원생 수준에 위치한다. 즉, 알려진 기법에는 능숙하지만 창의성이 요구될 때는 어려움을 겪는다.

이 연구가 당신의 연구에 주는 의미

수학적 추론을 연구하는 AI 연구자에게 RLMEval은 현재 역량에 대한 가장 솔직한 평가를 제공한다. 경시대회 벤치마크는 발전을 측정하는 데 유용하지만, 진정한 수학 연구 역량에 근접했다는 오해를 불러일으킨다. 격차는 크며, 이를 좁히려면 현재의 아키텍처가 지원하지 못할 수도 있는 창의적 추론의 발전이 필요하다.

수학자에게 RLMEval은 기대치를 조율해 준다. AI 증명 보조 도구는 일상적인 증명 작업에서 실질적인 도움을 줄 수 있으며, 인간의 노력을 창의적 작업에 집중시킬 수 있다. 그러나 경시대회 문제에서의 주목할 만한 결과를 연구 수학으로 외삽해서는 안 된다. 수학 연구의 창의적 핵심은 지금까지는 여전히 인간 고유의 영역으로 남아 있다.

수학 공동체 전반에 대해 RLMEval은 수학적 연구가 진정으로 무엇인지에 대한 질문을 제기한다. 일상적인 보조 정리가 자동화되고 경시대회 문제가 풀릴 수 있다면, 수학에 대한 인간 고유의 기여는 현재의 AI 시스템이 수행할 수 없는 추측, 전략 선택, 개념적 통찰이라는 창의적 행위에 점점 더 집중된다.