遇见数据集

Buchilaguo/Numina-ATF

收藏
Hugging Face2025-10-22 更新2025-10-25 收录
官方服务:

资源简介:

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
二维码
社区交流群
二维码
科研交流群
商业服务