Theorem Proving · AI-MO
GeometryLeanBench
A Lean 4 geometry theorem proving benchmark for automated reasoning and mathematics research.
What GeometryLeanBench is
GeometryLeanBench is a benchmark developed by AI-MO to evaluate automated reasoning and formal mathematics systems. It consists of formalised geometry problems designed to test theorem proving algorithms.
The dataset covers Euclidean, affine, and metric geometry. By providing formal statements in the Lean 4 proof assistant language, it offers a standardised target for evaluating scientific reasoning models on geometric proofs.
How it was made
The benchmark provides text-based problem representations formalised in the Lean 4 theorem proving environment.
Key facts
- Formalisation language
- Lean 4
- Geometry subfields
- Euclidean, affine, and metric geometry
- Format
- JSON
- Modality
- Text
What you can use it for
- Automated theorem proving evaluation
- Benchmarking the capacity of neural and symbolic theorem provers to complete formal geometric proofs.
- Scientific reasoning evaluation
- Assessing machine learning models on formal deductive logic across Euclidean, affine, and metric domains.
- Lean 4 proof generation testing
- Measuring model performance specifically when generating code and proof steps for the Lean 4 environment.
Explore the data
No licence declared
The authors have not published a licence, which means no permission to redistribute the data has been granted to anyone. The rows are not served here; read them on the original dataset page.How the columns are distributed
Over 122 rows of default/train
formal_statement
string_text- min
- 167
- median
- 395.50
- mean
- 435.76
- max
- 1,301
instruction
string_text- min
- 271
- median
- 499.50
- mean
- 539.76
- max
- 1,405
name
string_text- min
- 6
- median
- 11
- mean
- 15.87
- max
- 45
natural_language
string_label- 100%
statement_id
string_text- min
- 36
- median
- 36
- mean
- 36
- max
- 36
system
string_label- You are an expert in mathematics and proving theorems in Lean 4.100%
uuid
string_text- min
- 36
- median
- 36
- mean
- 36
- max
- 36
Strengths and limits
Good at
- Targets multiple mathematical domains by covering Euclidean, affine, and metric geometry.
- Employs Lean 4 to enable rigorous and verifiable theorem checking.
- Packaged in standard JSON text format for accessibility with common analysis tools.
Watch out for
- Requires tooling and evaluation workflows compatible with the Lean 4 proof assistant.
Questions
Can I look inside GeometryLeanBench without downloading it?
Not here: it declares no licence, so no permission to redistribute its rows has been granted. Its description and statistics are still shown.
What licence is GeometryLeanBench under?
Its authors have not declared a licence, which means no permission to reuse or redistribute it has been granted.
Which mathematical disciplines does this benchmark address?
It addresses theorem proving within Euclidean, affine, and metric geometry.
Which proof assistant is required to run these problems?
The problems are formalised specifically in Lean 4.
What file format is used for distribution?
The data is distributed in text-based JSON format.
Written from GeometryLeanBench's own dataset card. Statements citing a figure that does not appear there are removed before publication. Licence and running details come from our registry.