1. Astra가 한 일
8월 초 OpenAI가 10개의 수학 증명을 GitHub에 공개했다. 249페이지의 논문도 함께다[1]. 라이선스는 Apache 2.0이다[2]. 이 증명들은 Lean 4라는 도구로 작성되었다.
Lean 4는 수학 증명을 컴퓨터가 한 줄 한 줄 검증하는 소프트웨어다. 사람의 판단이 아니라 기계의 논리로 맞고 틀림을 확인한다. 공개된 저장소에 "sorry"라는 표시가 단 하나도 없다. sorry는 Lean에서 "이 부분은 아직 증명하지 못했다"는 뜻이다. 0개라는 것은 전 단계가 빈틈없이 검증되었다는 뜻이다[2].
풀어낸 문제들의 분야가 다양하다. 군론과 폰 노이만 대수, 고차원 기하학이 셋이다. 양자 복잡도, 격자 암호, 극값 조합론이 나머지다[2].
가장 주목받는 결과는 비소픽 군의 최초 명시적 구성이다[2]. 미하일 그로모프가 1999년 소픽성 개념을 제시했다. 그 뒤 27년간 아무도 답하지 못했다. 비소픽 군이 존재하는지를 증명도 반증도 못 했다[2].
두 번째는 콘느 강성 추측의 반증이다[2]. 이 추측은 이렇게 묻는다. property (T)를 갖는 군 G가 있다. 거기서 만든 폰 노이만 대수 L(G)가 G를 복원할 만큼의 정보를 담고 있는가. Astra는 반례를 만들어 반증했다. 같은 폰 노이만 대수를 공유하면서 서로 동형이 아닌 property (T) 군을 무한히 많이 구성했다[2].
나머지도 가볍지 않다. 에르하르트 부피 추측을 증명했다. 에르되시 문제 목록에서 세 문제를 풀었다. 그중 183번은 다색 램지 수에 관한 것이다[2].
비용이 놀랍다. 이 10개의 문제를 푸는 데 든 연산 비용은 약 2,000달러다[3]. 약 270만 원이다. 인간 수학자 팀이 수십 년간 매달린 문제다. 그것을 AI가 270만 원어치 컴퓨터 자원으로 풀었다.
2. Task AI에서 Research AI로
이 사건이 중요한 이유는 AI의 역할이 바뀌고 있기 때문이다.
지금까지 AI는 주로 Task AI였다. 주어진 업무를 자동화하는 것이다. 이메일을 요약하고 코드를 쓰고 고객 문의에 답한다. 사람이 시킨 일을 더 빠르고 싸게 처리하는 것이 핵심이었다.
Astra가 보여준 것은 다르다. 사람이 시킨 일을 한 것이 아니다. 사람이 풀지 못한 문제를 스스로 풀었다. 이것이 Research AI다. 기존에 없던 지식을 만들어내는 AI다.
이 구분이 왜 중요한가. Task AI는 기존 업무의 효율을 높인다. Research AI는 새로운 가능성을 연다. Task AI는 비용을 줄인다. Research AI는 매출을 만들 수 있다. 두 가지는 기업에 미치는 영향이 근본적으로 다르다.
Astra만 이런 것이 아니다. 2026년 5월에도 비슷한 일이 있었다. OpenAI의 내부 모델이 에르되시 단위거리 추측을 반증했다. 80년간 풀리지 않던 문제다[4]. 무한한 반례 집합을 제시해 다항식 수준의 개선을 얻었다[4].
수학자들의 반응이 이 사건의 무게를 보여준다. 필즈상 수상자 팀 가워스가 이렇게 썼다[5]. "단위거리 문제의 해결이 AI 수학의 이정표라는 데는 의심의 여지가 없다." 수학자 대니얼 리트는 더 나아갔다. 그는 이렇게 평가했다[5]. "AI가 자율적으로 만들어낸 결과 중, 앞날의 조짐이 아니라 그 자체로 흥미롭다고 느낀 최초의 사례다."
가워스의 첫 반응은 다른 의미로 인상적이다. 그는 처음에 AI가 이 추측을 증명했다고 잘못 들었다. 저녁 내내 세계관을 조정했다. 다음 날 아침 반증이었다는 것을 알고 안도했다고 밝혔다[5]. 증명이었다면 수학의 지형이 훨씬 크게 흔들렸을 것이라는 뜻이다.
Google도 같은 방향으로 움직인다. Gemini Deep Think가 수학적 난제를 다루고 있다. AlphaEvolve는 67개 문제에서 시험받았다[6]. 해석학과 조합론, 기하학, 정수론에 걸쳐 있다. 75%에서는 알려진 최선의 구성을 다시 찾았다. 20%에서는 기존 최고 기록을 넘는 새 대상을 찾아냈다[6]. AlphaEvolve는 Google이 만든 수학 탐색 에이전트다.
3. 기업 R&D에 미치는 영향
Research AI가 수학에서만 작동하는 것은 아니다. 이미 다른 분야로 확산되고 있다.
제약 분야에서는 AI가 신약 후보 물질을 제안한다. 단백질 간 상호작용도 예측한다. 임상 전 단계의 약물 특성을 시뮬레이션한다. AI 신약 개발 시장은 2026년 80~100억 달러가 될 전망이다[7]. 10년이 걸리던 일정이 수년으로 줄고 있다.
금융 분야에서도 변화가 시작되었다. 여신 심사에서 AI 에이전트가 리스크를 평가한다. 차주의 재무제표와 산업 동향, 과거 거래 이력을 함께 본다. 기존에는 심사역이 며칠에 걸쳐 하던 일이다. Research AI 수준의 추론 능력이 결합되면 달라진다. 데이터를 정리하는 것을 넘어선다. "이 차주의 산업이 향후 3년간 어떤 구조적 변화를 겪을 것인지"를 추론하는 단계로 갈 수 있다.
CRM 분야에서도 마찬가지다. CRM은 고객 관계 관리 시스템이다. 지금의 AI 기반 CRM은 고객 이탈 징후를 감지한다. 제품을 추천하고, 서비스 이슈 전에 먼저 연락하자고 제안한다[8]. Research AI가 결합되면 탐색이 가능해질 전망이다. "이 고객 군의 행동 패턴에서 아직 발견되지 않은 세그먼트가 있는가"를 묻는 일이다. 패턴을 인식하는 것과 발견하는 것은 차원이 다른 문제다.
4. 아직 넘어야 할 산
Research AI가 만능은 아니다. 냉정하게 봐야 할 것들이 있다.
첫째, 수학은 AI에게 유리한 영역이다. 증명이 맞는지 틀린지를 기계적으로 확인할 수 있기 때문이다. Lean 4가 이 역할을 한다. 그러나 금융 분석이나 경영 의사결정은 다르다. "맞다/틀리다"를 기계로 판별하기 어렵다. 정답이 없는 영역에서는 Research AI의 신뢰성이 검증되지 않았다.
둘째, MIT의 Project NANDA가 조사를 내놓았다. 2025년 8월이다. 기업의 생성형 AI 파일럿 중 95%가 손익에 영향을 내지 못했다[9]. 근거는 셋이다. 임원 52명 인터뷰, 리더 153명 설문, 도입 사례 300건 분석이다[9]. 기업들이 300~400억 달러를 쓴 뒤에 나온 숫자다[9].
MIT의 결론이 중요하다. 모델이 약해서 실패한 것이 아니다. 조직이 도입을 잘못 관리해서 실패했다[9]. Research AI도 같은 함정에 빠질 위험이 있다. 성능이 아무리 올라가도 도입 방식이 그대로면 결과는 같다.
셋째, 규제 환경이 변하고 있다. EU AI Act가 2026년 8월 2일 전면 시행되었다. 미국 FDA도 AI 지침을 2026년 내 확정할 전망이다[7]. 신약 개발이나 금융 심사에 AI가 끼면 판단 과정의 투명성이 요구된다. Research AI가 "새로운 발견"을 했다고 주장한다면 어떤가. 왜 그 결론에 닿았는지 설명할 수 있어야 한다.
JK's Take
Astra가 보여준 것은 모델의 도약이 아니라 검증 장치의 힘이다.
Astra가 수학에서 성공한 것은 Lean 4가 있었기 때문이다. 기계가 맞고 틀림을 판별해 준다. 그래서 AI가 스스로 시행착오를 걸러낼 수 있었다. 그 장치가 없는 영역에서 같은 성과를 기대하기는 어렵다.
그래서 기업이 물을 것은 어떤 모델을 쓸까가 아니다. "우리 R&D에서 AI가 발견할 수 있는 것은 무엇인가"다.
금융에서는 여신 심사의 패턴이거나 리스크 예측의 변수, 고객 이탈의 숨은 원인일 수 있다. 제조에서는 공정 최적화의 새 조합이거나 소재 특성의 미발견 관계다.
다만 순서가 있다. 온톨로지 설계와 지식그래프 구축, 데이터 품질 관리가 기업의 Lean 4다. 이것 없이 Research AI를 들이면 모델만 바꾼 것이 된다.
AI가 연구를 하는 시대가 왔다. 그러나 연구할 수 있는 데이터를 가진 기업만이 그 혜택을 누릴 것이다.
What to Watch
— Astra의 공개 출시 시점과 사양을 주목하라. 지금은 내부 버전만 있다. 미국 정부의 사전 심사를 거쳐야 출시된다. API로 풀리는 순간 Research AI는 사서 쓰는 물건이 된다. 차별점은 모델에서 데이터로 옮겨간다.
— Research AI의 수학 외 적용 사례를 추적하라. 생물학과 금융, 소재 과학으로 얼마나 빨리 번지는가. 그것이 실제 가치를 말해 준다. 정답을 기계로 판별할 수 없는 영역에서도 작동하는지가 관건이다.
— 자사 데이터의 구조화 수준을 점검하라. 지식그래프와 온톨로지, 데이터 품질 관리가 어디까지 되어 있는가. 그것이 Research AI를 쓸 수 있는 기업과 못 쓰는 기업을 가른다.
References
[1] TechTimes, "OpenAI's Astra Solves Ten Decade-Old Math Problems With Machine-Checkable Lean Proofs", 2026-08-02. https://www.techtimes.com/articles/322710/20260802/openais-astra-solves-ten-decade-old-math-problems-machine-checkable-lean-proofs.htm — Lean 4는 수학 증명을 형식화하고 컴퓨터가 검증하는 소프트웨어다. 증명 코드를 실행하면 "통과" 또는 "실패"를 자동 판별한다.
[2] SiliconANGLE, "OpenAI's Astra solves 10 long-open math problems and publishes the proofs", 2026-08-02. https://siliconangle.com/2026/08/02/openais-astra-solves-10-long-open-math-problems-publishes-proofs/ — 249페이지 원고와 Lean 4 증명 인증서를 GitHub에 Apache 2.0 라이선스로 공개. 저장소의 "sorry" 개수는 0으로, 10개 증명의 모든 단계가 검증됐다. "sorry"는 Lean에서 아직 증명하지 못한 부분을 임시로 넘어갈 때 쓰는 표시다. 결과는 군론, 폰 노이만 대수, 고차원 기하학, 양자 복잡도, 격자 암호, 극값 조합론에 걸쳐 있다. 대표 성과는 비소픽 군의 최초 명시적 구성으로, 미하일 그로모프가 1999년 소픽성을 제시한 이후 27년간 미해결이었다. 콘느 강성 추측은 같은 폰 노이만 대수를 공유하는 비동형 property (T) 군을 무한히 구성해 반증했다. 그 밖에 에르하르트 부피 추측 증명, 에르되시 문제 3건(다색 램지 수를 다루는 183번 포함) 해결.
[3] Yahoo Tech, "OpenAI Astra model solves 10 open math problems for $2,000", 2026-08. https://tech.yahoo.com/ai/articles/openai-astra-model-solves-10-124919950.html — 연산 비용 약 2,000달러. OpenAI의 Sol API 가격 기준 환산치로, 실제 내부 연산 비용은 다를 수 있으나 규모감을 보여주는 수치다.
[4] OpenAI, "An OpenAI model has disproved a central conjecture in discrete geometry", 2026-05. https://openai.com/index/model-disproves-discrete-geometry-conjecture/ — 내부 모델이 80년간 미해결이던 에르되시 단위거리 추측을 반증했다. 무한한 반례 집합을 제시해 다항식 수준의 개선을 얻었다.
[5] Understanding AI, "OpenAI's math breakthrough played to AI's strengths", 2026. https://www.understandingai.org/p/openais-milestone-math-breakthrough — 팀 가워스(1998년 필즈상)는 "단위거리 문제의 해결이 AI 수학의 이정표라는 데는 의심의 여지가 없다"고 평가했다. 대니얼 리트는 "AI가 자율적으로 만들어낸 결과 중, 앞날의 조짐이 아니라 그 자체로 흥미롭다고 느낀 최초의 사례"라고 썼다. 가워스는 처음 증명으로 잘못 전해 듣고 저녁 내내 세계관을 조정했다가 다음 날 반증임을 알고 안도했다고 밝혔다. ※ "그 자체로 흥미로운 최초의 사례"는 가워스가 아니라 리트의 발언이다.
[6] Google DeepMind, "AlphaEvolve: A coding agent for scientific and algorithmic discovery", arXiv:2506.13131. https://ar5iv.labs.arxiv.org/html/2506.13131 — 해석학·조합론·기하학·정수론에 걸친 67개 문제에서 시험. 75%에서 알려진 최선의 구성을 재발견하고, 20%에서 기존 최고를 넘어서는 새로운 대상을 발견했다. AlphaEvolve는 LLM이 후보 코드를 제안하고 자동 평가와 반복 진화 루프로 개선하는 구조다.
[7] Drug Target Review, "AI in drug discovery: predictions for 2026", 2026. https://www.drugtargetreview.com — AI 신약 개발 시장 규모 80~100억 달러는 시장 조사 기관의 2026년 전망치다. FDA의 AI 지침은 2026년 내 최종 확정될 예정이다.
[8] CX Today, "Financial Services CRM Gets an AI Overhaul across Salesforce, Anthropic and CSI", 2026. https://www.cxtoday.com — AI 기반 CRM은 행동 신호를 감지하고, 잠재적 이탈을 탐지하고, 제품을 추천하고, 서비스 이슈 전에 선제적 연락을 제안하는 수준으로 발전했다.
[9] MIT Project NANDA, "The GenAI Divide: State of AI in Business 2025", 2025-08. https://www.aigl.blog/state-of-ai-in-business-2025/ — 임원 52명 인터뷰, 리더 153명 설문, 공개 AI 도입 사례 300건 분석. 기업이 300~400억 달러를 투입했으나 생성형 AI 파일럿의 95%가 손익에 측정 가능한 영향을 내지 못했다. 통합된 파일럿 중 5%만이 수백만 달러 규모의 가치를 뽑아내고 있다. MIT는 원인을 모델 성능이 아니라 조직의 도입 관리 실패로 지목했다.
— 2026-09-07 업데이트: 미주 9개 전체에 원문 링크를 추가하고 2차 출처를 원 발표처로 교체했다. 같은 점검에서 "AI가 자율적으로 만들어낸 결과 중 그 자체로 흥미로운 최초의 사례"라는 발언이 팀 가워스가 아니라 대니얼 리트의 것임을 확인해 2장을 수정했다. 가워스의 실제 발언은 별도로 인용했다. MIT 95% 수치의 출처를 2차 블로그에서 MIT Project NANDA 원 보고서로 바꾸고 조사 방법을 명시했다. 1장에는 Apache 2.0 라이선스, 그로모프의 1999년 소픽성 제시 이후 27년이라는 경과, 에르하르트 부피 추측과 에르되시 183번 등 확인된 세부를 보강했다.