ruc-ai4math/mathlib_handler_benchmark_410
This dataset is used in the paper Assisting Mathematical Formalization with A Learning-based Premise Retriever. It contains data for training and evaluating a premise retriever for the Lean theorem prover. The dataset is described in detail in the GitHub repository. It consists of proof states and corresponding premises from the Mathlib library. The data is designed to train a model to effectively retrieve relevant premises for a given proof state, assisting users in the mathematical… See the full description on the dataset page: https://huggingface.co/datasets/ruc-ai4math/mathlib_handler_benchmark_410.
This dataset is used in the paper Assisting Mathematical Formalization with A Learning-based Premise Retriever. It contains data for training and evaluating a premise retriever for the Lean theorem prover.
The dataset is described in detail in the GitHub repository. It consists of proof states and corresponding premises from the Mathlib library. The data is designed to train a model to effectively retrieve relevant premises for a given proof state, assisting users in the mathematical formalization process. The dataset is available for download at this link.