NuminaMath-LEAN은 Numina와 Kimi 팀이 2025년에 공동으로 발표한 수학 문제 데이터 세트입니다. 관련 논문 결과는 다음과 같습니다.Kimina-Prover 미리보기: 강화 학습을 통한 대규모 형식 추론 모델 구축"는 자동화된 정리 증명 모델의 훈련과 평가를 위해 수동으로 주석이 달린 공식적인 진술과 증명을 제공하는 것을 목표로 합니다.

이 데이터셋에는 국제수학올림피아드(IMO) 및 미국수학올림피아드(USAMO)와 같은 권위 있는 대회의 문제를 포함하여 10만 개의 수학 경시대회 문제가 포함되어 있습니다. 데이터 유형에는 문제 진술, 문제 유형 분류, 정답, 출처, 정형 증명, 주석자 정보, 강화 학습 학습 과정 기록 등이 포함됩니다.