---
title: "Lean-IMO-Bench"
created: 2026-07-03
updated: 2026-07-03
type: concept
tags: ["benchmark", "imo", "lean", "formal-verification"]
sources: ["arxiv:2606.03303"]
---

# Lean-IMO-Bench

> 将 IMO 级别问题形式化到 Lean 中的新基准——初等陈述、非平凡洞察、长链多步证明。

## 核心定义

**Lean-IMO-Bench** 是 [[leap-agentic-atp|LEAP]] 论文中引入的基准，基于 IMO-Bench (Luong et al., 2025) 的非形式化问题，由 Lean 专家手动形式化为 Lean 声明。共 60 题，均分 Basic 和 Advanced 各 30 题。

## 与现有基准的对比

| 基准 | 特点 | 饱和程度 |
|------|------|---------|
| MiniF2F | 短问题 | 接近饱和 |
| PutnamBench | 本科覆盖面广 | - |
| **Lean-IMO-Bench** | 初等陈述，多步非平凡证明 | 远未饱和 |

## 基准结构

- **Basic Set (30 题)**：pre-IMO 到 IMO-Medium，含 8 代数、8 组合、8 数论、6 几何
- **Advanced Set (30 题)**：新颖问题至 IMO-Hard，含 8 代数、8 组合、6 数论、8 几何

## 三个评估任务

1. Natural Language Proof（非形式化证明）
2. Formal Theorem Proving（形式化定理证明，本文焦点）
3. Formal Proof Translation（非形式化 → 形式化翻译）

## 基线表现

- Gemini 2.5 Pro 非形式化证明：Basic 55.2%，Advanced 17.6%
- Gemini 3.1 Pro 形式化证明 (Pass@128)：Basic 20%，Advanced 3.3%——数学推理不是瓶颈，生成有效 Lean 代码是

## 参考

- [[leap-agentic-atp|LEAP]]
- [[formal-theorem-proving|形式化定理证明]]
- [[lean-proof-assistant|Lean 证明助手]]