# Mo Int 20 Eval

> 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.

- Skill: `qhjqhj00/mo-int-20-eval` (Agent Skill)
- Install (CLI): `npx skillmds add qhjqhj00/mo-int-20-eval`
- Raw SKILL.md: https://api.skillmd.com/api/skills/qhjqhj00/mo-int-20-eval/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Productivity
- Author: qhjqhj00 (https://skillmd.com/u/qhjqhj00)
- Updated: 2026-09-08
- Page: https://skillmd.com/skills/qhjqhj00/mo-int-20-eval

---


# 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