Mo Int 20 Eval

---
name: mo-int-20-eval
description: Evaluates the ability of automated theorem provers and LLMs to formally prove complex algebraic inequalities at the International Mathematical Olympiad level using a deductive search engine in Lean. Use when the user wants to benchmark on MO-INT-20, or asks about evaluating this task. Reports number of solved problems.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 2406.14219
  bibtex_key: [REDACTED]
  confidence: high
---

# mo-int-20-eval

> Proving Olympiad Algebraic Inequalities without Human Demonstrations — Wei et al. (2024) (arXiv:2406.14219, 2024)

## What this evaluates

Evaluates the ability of automated theorem provers and LLMs to formally prove complex algebraic inequalities at the International Mathematical Olympiad level using a deductive search engine in Lean.

## Datasets

- **MO-INT-20** — total 20; splits: test (20)

## Metrics

- `number of solved problems` **(primary)** — range: other
  - Count of problems successfully proven within the 90-minute time limit out of the total 20 problems.

## Input / output format

**Input**: Algebraic inequality problems translated into Lean formal language.

**Output**: A complete formal proof in Lean that successfully verifies the inequality.

## Scoring recipe

```python
solved_count = 0
for problem in test_set:
    proof = prover.generate_proof(problem, time_limit=90*60)
    if lean_verify(proof) == "success":
        solved_count += 1
return solved_count
```

## Common pitfalls

- Problems are strictly limited to a 90-minute solving time per instance.
- LLM-based provers may fail due to context length limits when expression trees grow too large during search.
- Training data contamination is a concern, though authors verified test problems are absent from training sets.

## Evidence (verbatim from paper)

> We evaluate AIPS on an Olympiad-level algebraic inequality problem test set. It outperforms the state-of-the-art methods in terms of the number of solved problems, demonstrating the strong algebraic intuitions developed by the learned value network.

## Citation

```bibtex
@misc{wei2024provingolympiad,
  title={Proving Olympiad Algebraic Inequalities without Human Demonstrations},
  author={Wei et al. (2024)},
  year={2024},
  note={arXiv:2406.14219}
}
```

- arXiv: 2406.14219