Buchilaguo/Numina-ATF
收藏Hugging Face2025-10-22 更新2025-10-25 收录
下载链接：
https://hf-mirror.com/datasets/Buchilaguo/Numina-ATF
下载链接
链接失效反馈官方服务：
资源简介：
Numina-ATF是NuminaMath-1.5的LEAN 4版本，包含了753K高质量的数学定理的非正式和正式表述对。每个数学查询在经过ATF-32B正式化后，都进行了语法和语义一致性的验证。LEAN 4版本使用的是v4.9。
Numina-ATF is the LEAN 4 formalized version of NuminaMath-1.5, containing 753K high-quality informal-formal pairs of mathematical theorems. Each mathematical query is verified for syntactic and semantic consistency after being formalized by ATF-32B. The LEAN 4 version uses v4.9.
提供机构：
Buchilaguo
