Datasets › RLM25
RLM25 (Research-Level Mathematics 2025)
RLM25 is an evaluation benchmark containing 619 paired examples of research-level natural language mathematical statements and their corresponding Lean formalizations. The examples are drawn from six real-world formalization projects, and each entry includes essential context along with timestamp information to ensure freshness and avoid data contamination. Its primary purpose is to serve as a challenging testbed for assessing autoformalization systems, helping researchers measure improvements in translating complex, research-level mathematics into formal code.
Benchmarks archive 2025-07-28
No leaderboard in the archive resolves to this dataset.
Papers archive 2025-07-28
No paper in the archive has a leaderboard row on this dataset; the archive counts 1 paper for it but never published that list.
Dataset loaders archive 2025-07-28
No loader listed in the archive.
Tasks archive 2025-07-28
License archive 2025-07-28
No licence recorded in the archive. Absence here is not a statement about the dataset's terms.
Modalities archive 2025-07-28
Languages archive 2025-07-28
Variants archive 2025-07-28
- RLM25
1 variant name, as the archive lists them.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections