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.