여러 시스템의 비교
같은 수학적 문제라도 증명 시스템마다 표현이 다를 수 있다. miniF2F는 시스템을 넘는 통합 평가를 목표로 형식적인 문제 명세를 모았다.
경시와 교육 과정의 문제
초기 자료는 AIME와 AMC, 국제수학올림피아드 및 고등학교와 대학 수학 과정의 문제를 포함했다. 단일 라이브러리 안의 정리만이 아니라 다양한 수준의 수학 문제를 다룬다.
초기 대상 시스템
소개 논문은 Metamath와 Lean을 대상으로 하고 Isabelle과 HOL Light도 일부 지원한다고 설명했다. 여러 시스템을 목표로 한다는 것과 모든 문제의 형식화가 동일하게 갖춰졌다는 것은 구별된다.
기준 모델과 공동체
초기 연구는 GPT-3 기반 신경 증명기 GPT-f의 결과와 분석을 제시했다. 공동체가 함께 발전시키는 평가로 신경망 기반 정리 증명 연구를 지원하려는 자료다.
관련 문서
Lean 증명 도구 / LeanDojo / Mathlib / HOList / MATH 수학 평가 / 논리학