Readme

이 저장소에는 내부 OpenAI 모델이 생성한 수학 원고 및 지원 증명 아티팩트가 포함되어 있습니다.

모델 개발의 일환으로, 우리는 개방된 연구 문제에 대해 모델을 평가합니다. 기존 수학적 평가에서 성능 포화 상태에 도달함에 따라 이러한 평가는 확장되었습니다. 일부 출력물은 모델이 이전에 생성한 결과를 기반으로 구축되었습니다.

이 컬렉션에는 다양한 검증 단계의 결과가 포함되어 있습니다. 모든 결과에 동반되는 Lean 형식화(formalization)는 없습니다. 저희가 확보하는 대로 이 저장소에 Lean 형식화를 계속 업데이트할 것입니다.

형식화되지 않은 일부 결과에는 문제가 있을 수 있습니다. 저희는 그러한 문제를 신속하게 수정하기 위해 노력할 것입니다.
저희는 또한 이러한 자료를 위한 커뮤니티 호스팅 저장소를 탐색하고 있습니다.

컬렉션 탐색

현재 카탈로그에는 372개의 패밀리(family)로 구성된 722개의 원고가 포함되어 있습니다. 하나의 패밀리는 주요 결과, 보조 논증, 결과, 또는 대체 증명을 포함할 수 있는 관련 논문들을 그룹화합니다. 각 패밀리는 수학적 학문 분야별로 분류됩니다.

• 패밀리 설명은 overview에서 시작하십시오.
• 개별 논문과 지원 자료를 찾으려면 manuscript map을 사용하십시오.
• preprints/ 디렉터리에는 PDF, 소스 파일, 원고별 인용 및 빌드 지침이 포함되어 있습니다.
• Lean 라이브러리와 형식화 카탈로그는 사용 가능한 형식 증명, 관련 논문, 그리고 검증 구성을 설명합니다. 추가적인 확인 지침은 Comparator instructions를 참조하십시오. 원고의 상당수는 형식화되었지만, 모든 것이 그렇지는 않습니다.

추론 요약

저희는 또한 다음 결과를 다루는 모델의 추론에 대한 간략한 요약을 공개하고 있습니다:

추론 요약

저희는 또한 다음 결과를 다루는 모델의 추론에 대한 간략한 요약을 공개하고 있습니다:

결과 도출 과정

대부분의 결과는 공개되지 않은 내부 OpenAI 모델을 사용하여 동일한 절차로 얻어졌습니다. 평균적으로, 각 결과를 산출하는 데 해당 모델을 이용해 3시간 분량의 ChatGPT Pro 사고 컴퓨팅이 사용되었습니다. 평가 기간 동안 이 모델은 약 4,000개의 문제에 직면했습니다. 출력물을 결과 패밀리 및 원고로 통합하고 적절한 유의 수준을 요구하면서 위의 카탈로그가 작성되었습니다.

이 고정된 절차의 예외에는 리만 제타 함수(Riemann zeta function)의 영점 자유 영역(zero-free region)에 대한 작업과 CM 아벨 다양체(CM abelian varieties)에 대한 호지 추측(Hodge Conjecture) 증명이 포함됩니다. 또한, 리만 제타 함수의 Re(s) > 11/12 영점 자유 영역에 대한 기록은 가독성을 위해 사람이 편집했습니다.

버전 및 인용

저희는 이 컬렉션의 공개된 출시 이력을 보존할 것입니다. 수정 및 개정 사항은 새로운 버전으로 기록되며, 이전에 발표된 버전들은 계속 접근 가능합니다.

개별 원고를 인용하려면 해당 디렉터리 내의 BibTeX 블록을 사용하십시오.