# OpenAI의 차기 핵심 AI 모델 “아스트라”가 10건의 수학 및 이론 계산 과학 과제에서 새로운 성과와 증명을 Lean 4에서 형식화하여 기계 검증 가능하게 함

> https://bookfactory.kr/c/news/8802
> 게시판: 뉴스
> 작성자: tachikoma43
> 작성일: 2026-08-03T03:46:04.777Z

---

OpenAI는 2026년 8월 1일, 차기 핵심 AI 모델 “Astra”의 내부 버전을 통해 수학과 이론적 컴퓨터 과학 분야에서 10건의 미해결 과제에 새로운 성과를 거두었다고 발표했습니다. 이 과제들은 “주요 결론에 대해 최소 10년 이상 진전이 없었던 문제”로, OpenAI는 249페이지 분량의 논문과 증거를 기계적으로 검사할 수 있는 데이터를 공개했습니다.

OpenAI는 모델의 수학 능력을 시험 문제뿐만 아니라 미해결 연구 과제에서도 평가하도록 하고 있습니다. OpenAI는 2026년 5월에도 수학자 폴 엘데슈가 제안한 단위 거리 예측(Unit Distance Conjecture)을 비공개 모델이 반증했다고 보고했습니다. OpenAI는 80년 가까이 미해결이었던 수학 예측의 반증에 성공했으며, 인간 수학자들도 “AI가 보조 역할을 넘어섰다”고 놀라워하는 발견입니다.

이번 발표는 비공개 모델을 여러 분야의 미해결 과제에 참여시켜 얻은 결과 중 10건을 종합하여 공개하는 것입니다. OpenAI에 따르면 Astra가 생성한 수학적 논의는 인간 담당자들에 의해 논문 초안으로 정리되었고, 이후 Astra가 각 논의에 대해 정리된 논거와 전제 조건을 엄밀한 기호로 기술하여 추론 단계가 규칙에 따라 진행되는지 컴퓨터로 확인하는 소프트웨어 “Lean 4”로 형식화했습니다. GitHub에서 공개된 저장소에는 10건분의 Lean 형식의 증명 데이터에 더하여 증명 전체를 구축하는 절차와 독립 검사 도구 안내도 포함되어 있습니다.

OpenAI가 공개한 10가지 성과는 다음과 같다.

*   고차원의 구 충진 밀도 상한을 코른-엘키스법으로 얻어지는 限界値까지 개선
*   이원 부호와 球面 부호의 최대 규모에 대해 기존보다 지수 함수적으로 강한 상한을 유도
*   유한 대체로 근사할 수 없는 비소群을 구성
*   특정 군이 대응하는 군 폰 노이만 환에 의해 유일하게 결정된다는 콘누의 강성 예상에 대한 반례
*   행렬의 페르망트를 계산하는 산술 회로와 산술식에 대해 새로운 계산량 하한을 증명
*   양자 얽힘을 이용하는 임의의 유한한 2인 게임에 대해 지수 함수적인 병렬 반복 정리를 증명
*   최근 벡터 문제에 대해 격자의 차원에 대해 다항식 배수의 오차를 허용해도 근사가 어렵다는 것을 증명
*   중심만 내부 격자 점이 되도록 하는 凸体에 대해 에일하트의 체적 예상은 모든 차원에서 증명
*   다색 삼각형 람즈 수에 대해 초지수 함수적인 하한을 증명
*   극값 그래프 이론에 있어서 컴팩트성 예상과 퇴화도에 대한 예상에 각각 반례를 구성

이원 부호와 球面 부호에서는 고차원에서의 일반적인 상한을 각각 1977년과 1978년 이후 처음으로 개선한 것 외에, 구 충진에서도 일반적인 고차원 지수를 1978년 이후 처음으로 개선했다는 설명이다. 양자 계산량 이론에서는 동일한 게임을 병렬로 반복했을 때 모든 게임에 승리할 확률이 지수 함수적으로 감소하는 “병렬 반복 정리”를 양자 얽힘을 이용하는 임의의 유한한 2인 게임까지 확장했다.

해법 탐색에 필요했던 총 토큰 수를 OpenAI의 “Sol API” 요금에 적용하면 약 2,000달러(약 31만 원)가 소요되었다고 한다. OpenAI는 원래 사고 과정의 기록이나 완성된 논문 등을 다른 AI 모델에 읽어주어 증명에 이르는 과정을 재구성한(PDF 파일) 설명 자료도 공개했다. 설명 자료는 원래 사고 과정의 기록을 그대로 게시한 것이 아니라, 실패한 방향이나 시각의 전환, 최종적인 착상을 읽기 쉬운 설명으로 정리한 것이다. 한편, “수학 AI의 보급 이후에도 인간이 기존과 같이 수학을 지속할 수 있다는 보장은 없다”고 주장하는 논고도 등장했다. 논고에서는 수학은 과학이나 공학에 응용되는 분야이므로 체스처럼 닫힌 활동이 아니며, AI가 인간의 이해를 거치지 않고 수학·과학·공학을 발전시킬 가능성이 있다고 논지되고 있다.

OpenAI는 수학적 논의 자체를 Astra가 생성했다는 점을 명시하며, 논문 초안 작성과 Lean을 통한 형식화에 관여한 OpenAI가 증명의 정확성에 대한 책임을 지고 있다고 밝혔습니다. Astra 자체의 공개 전에 10개의 증명이 공개된 형태로, 앞으로 수학계는 각 성과를 기존 연구 안에 위치시키고 새로운 연구로 연결되기를 기대하고 있다고 합니다.

[원문 보기](https://gigazine.net/news/20260803-openai-astra-lean/) | 출처: Gigazine