datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
IMO-Lemmas
Tencent-IMO: Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
This dataset contains strategic subgoals (lemmas) and their formal proofs for a challenging set of post-2000 International Mathematical Olympiad (IMO) problems. All statements and proofs are formalized in the Lean 4 theorem proving language.
The data was generated using the Decoupled Reasoning and Proving framework, introduced in our paper: Towards Solving More Challenging IMO Problems… See the full description on the dataset page: https://huggingface.co/datasets/Tencent-IMO/IMO-Lemmas.hellenistic-greek-lemmas
Dataset Card for "hellenistic-greek-lemmas"
More Information needed
tajik_lemmasLEMMA-Self-Fix-70Kimo-1969-p2-lemmasLean formalizations of lemmas for IMO 1969 Problem 2 from the BFS-Prover-V2 paper by Xin et. al
refined_roosterize_lemmasroosterize-lemmasscrambled_lemmas