ruc-ai4math/mathlib_handler_benchmark_410
收藏Hugging Face2025-03-07 更新2025-04-19 收录
下载链接：
https://hf-mirror.com/datasets/ruc-ai4math/mathlib_handler_benchmark_410
下载链接
链接失效反馈官方服务：
资源简介：
该数据集包含了用于训练和评估Lean定理证明器前提检索器的证明状态和对应的前提数据，这些数据来自于Mathlib库。它旨在帮助用户在数学形式化过程中，通过检索相关前提来辅助证明。
This dataset contains proof states and corresponding premises for training and evaluating a premise retriever for the Lean theorem prover, sourced from the Mathlib library. It is designed to assist users in the mathematical formalization process by retrieving relevant premises to aid in proof construction.
提供机构：
ruc-ai4math
