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.
Dataset Structure
informal_statement: Mathematical problems expressed in natural language.
formal_statement: LEAN 4 formalized problems… See the full description on the dataset page: https://huggingface.co/datasets/Buchilaguo/Numina-ATF.
