AI 시대 수학자 평가에 문제 선택과 증명 이해를 반영하자는 칼레가리
시카고대 수학 교수 프랭크 칼레가리는 OpenAI의 2026년 10월 수학 결과 공개를 계기로, AI가 만든 증명뿐 아니라 문제 선택과 결과 이해, 후속 연구로 잇는 기여도 평가하자고 제안했습니다. 채용과 논문 심사, 대학원 교육을 연구자의 수학적 이해와 넓은 맥락 설명에 무게를 두는 방식으로 바꾸자는 개인 기고입니다.
AI · 최신기사
AI 모델과 서비스, 활용 도구와 이용 조건을 다룹니다.
Lean으로 형식화한 유한 단순군 분류
Axiom Math가 유한 단순군 분류의 1세대 증명을 Lean으로 완전히 형식화했다고 발표했습니다. 형식화 과정에서 불균형 군 정리의 기존 증명에 문제가 있음을 발견해 대안 증명을 제시했고, Lean 커널이 각 논리 단계를 검사합니다.
Anthropic 내부 Claude 연구 모델도 10월 16일 지수 시간 가설을 독자적으로 반박했습니다. 출력 토큰 1,400만 개, 인간 개입은 없었습니다
Anthropic의 내부 Claude 연구 모델이 3-SAT의 지수 시간 가설(ETH)을 반박하는 결과를 냈으며, 더 어려운 #3-SAT 계수 문제도 준지수 시간에 푸는 알고리즘을 제시합니다. Lean 4 형식화와 별도 커널 검증 절차도 공개했지만, 결과는 점근적이며 실제 문제 풀이 성능을 뜻하지 않습니다.
수학·컴퓨터과학·물리학에서 세 가지 발견 발표
OpenAI는 조화해석학, 계산복잡도론, 양자장론에서 세 가지 결과를 얻었으며 Lean 형식화 증명을 공개하거나 전문가 그룹과 검토 중이라고 밝혔습니다. 그중 ETH 반증과 양자색역학 존재 증명은 각 분야의 오래된 문제를 다루지만, 결과의 해석과 검증은 계속 진행될 예정입니다.
최근 제안된 o(n log n) 정수 곱셈 알고리즘
정수 곱셈의 기존 O(n log n) 시간 경계를 처음으로 o(n log n)으로 낮췄다는 알고리즘을, 기존 알고리즘의 저자인 David Harvey가 검토합니다. 직접 증명을 완전히 확인하지는 못했지만 AI의 설명을 바탕으로 주장이 그럴듯하다고 판단하며, 가속화 아이디어와 검증의 과제를 설명합니다.
AI가 준 리만 가설을 증명했습니다. 이제 무엇이 달라질까요?
OpenAI가 발표한 증명은 리만 제타 함수의 비자명한 영점이 놓이는 영역을 기존보다 좁혀 준 리만 가설을 증명합니다. 수론 전문가들은 오래된 결과와 아이디어를 새롭게 조합한 증명으로 보고 있으며, 소수 분포와 여러 수학 분야에 파급될 결과를 검토하고 있습니다.
OpenAI의 네이비어-스톡스 증명, 처음 알려진 접근과 달랐다
OpenAI의 Navier-Stokes 증명은 스페인 수학자들의 접근법을 그대로 따른 결과가 아니라, 세부 구조가 다른 방법을 사용한 것으로 전문가들이 파악하고 있습니다. 다만 대규모 LLM이 만든 Lean 증명과 논문 설명의 차이, 모델의 추론 경로를 확인하기 어려운 점은 남아 있습니다.
테렌스 타오의 ‘수학 2.0’ — 증명 풍요의 시대에 수학이 나아갈 길
테렌스 타오는 AI가 수학 문제의 증명을 빠르게 내놓는 ‘증명 풍요’ 시대에 문제 풀이만을 연구 목표로 삼으면 수학의 장기적 발전을 해칠 수 있다고 주장합니다. AI를 증명 생성에만 쓰기보다 인간의 이해와 새로운 연구 영역을 넓히는 데 활용하고, 평가 기준과 연구 관행도 바꿔야 한다고 제안합니다.
수학자가 Lean 정리 증명기에 알아야 할 것: 신뢰성과 AI
Thomas Hales는 Lean을 이용한 수학 형식화와 AI 자동 형식화의 진전을 소개하고, 증명 커널의 soundness bug와 Lean 형식 체계의 미해결 기초 문제를 짚습니다. 형식 검증 결과를 신뢰하려면 커널만 확인할 게 아니라 정리와 정의가 원래 의도와 일치하는지도 사람이 감사해야 한다고 강조합니다.
OpenAI, 수학 논문 3편 철회하고 14편 수정
OpenAI는 부호 오류로 핵심 논증이 무너진 논문과 그 결과에 의존한 논문 두 편을 철회했습니다. 다른 논문 14편도 증명과 가정 등을 수정했으며, 추가 수정본 인용과 형식화 결과를 반영해 주요 결과의 Lean 형식화 비율은 300/719, 약 42%가 됐습니다.
번역 과정에서 어긋난 나비에–스토크스 증명
이 논문은 자연어 수학 증명을 Lean으로 옮긴 뒤 검증해도 원래 증명이 충실하게 번역됐다는 보장은 없다고 설명합니다. 저자들은 의미를 보존하며 자연어의 모호성을 해소하는 일이 계산 복잡도 계층에서 정지 문제보다도 높은 수준에 이를 수 있다고 주장하고, OpenAI의 나비에–스토크스 증명에서도 두 표현이 맞지 않는 사례를 제시합니다.
AI가 만든 수학 연구 결과와 공개 방식
OpenAI가 내부 모델로 얻은 수학 결과를 GitHub에 공개하고, 일부 증명은 Lean 형식화 자료로 제공합니다. 추론 요약과 계산량 추정치도 공개했지만, Hacker News에서는 결과 검증과 수학계의 연구 관행을 둘러싼 논쟁이 이어집니다.
OpenAI Dots 에이전트 군집으로 47년 된 수학 하한을 높이다 — Lean으로 증명 검증
작성자는 OpenAI Dots의 에이전트 7개를 약 3일간 운용해 덮개수 문제 C(24,14,4)의 하한을 19에서 20으로 높였다고 보고합니다. 여러 에이전트의 교차 검토와 Lean 기계 검증을 거쳤지만, 수학자의 동료 검토는 아직 진행 중입니다.
애도할 것인가, 말 것인가?
수학 연구에서 AI가 어려운 문제를 풀기 시작하자 수학자들이 느끼는 상실감과 기대를 살핍니다. 저자는 수학의 가치를 ‘이해’ 하나로 설명하기 어렵다고 짚으며, 정리 증명·이론 구축·추측 제시를 나눠 AI의 현재 능력과 한계를 논하고 OpenAI에 비공개 수학 결과를 공개하라고 촉구합니다.
AI 생성 수학 결과를 책임 있게 공개하는 방법
AGMAI는 사람이 이해하지 못한 AI 생성 수학 결과를 연구소가 공개할 때 필요한 절차와 지원책을 제안합니다. 증명 정리와 선행 연구 인용, 프롬프트·계산 비용 공개, 형식 검증, 연구자 지원을 권고하며, 비공개 모델로 난제를 시험하지 말라고도 요청합니다. Hacker News에서는 수학의 개방성과 인간의 이해를 지킬 방안을 두고 찬반이 맞섰습니다.
FrontierMath, 아페리식 무리수성 문제를 해결로 표시
FrontierMath가 ζ(5)의 무리수성을 증명하는 해답을 확인해 문제를 해결로 표시했습니다. 해답은 문제에서 찾도록 한 아페리(Apéry)식 점화식을 사용하지 않으며, FrontierMath는 AI 시스템의 정체를 모르는 상태에서 인간과 AI가 함께 만든 결과로 판정했습니다.
수학자가 훨씬 더 많이 필요합니다
AI가 인간 연구자보다 빠르게 새로운 수학적 아이디어를 내놓는 시대에도, 사람이 그 결과를 이해하고 안전성과 타당성을 검토할 역량을 키워야 한다고 Amit Sahai가 주장합니다. 이를 위해 수학자 공동체를 확장하고, AI가 만든 발견을 함께 연구할 인력을 지원해야 한다고 제안합니다.
OpenAI는 나비에–스토크스 문제를 잘못 풀었을까요?
OpenAI가 푼 문제는 클레이 수학연구소의 공식 조건에는 들어맞지만, 외력을 쓰지 않는 나비에–스토크스 문제는 여전히 풀리지 않았습니다. 새 연구는 OpenAI의 방법이 외력을 제거한 문제에는 적용되지 않는다고 보이며, 수학적 성과의 의미를 둘러싼 논쟁도 이어집니다.
수학 및 인공지능 자문 그룹 출범
Institute for Advanced Study가 수학 연구와 AI 기업의 상호작용을 다룰 독립 자문 그룹을 출범합니다. 그룹은 OpenAI가 내부 모델로 얻었다고 밝힌 다수의 수학 결과를 어떤 방식으로 공개할지 조언하며, 회원 명단과 권한의 한계를 공개했습니다.
이제 인간 수학자가 왜 필요한가?
Po-Shen Loh는 AI 시대에도 인간 공동체와 전문성을 지켜야 한다는 원칙으로 ‘인류의 번영을 돕는다’를 제안합니다. AI가 통제해야 할 지점을 폭발적으로 늘리면 숙련된 인간 인력이 부족해지고, 결국 AI 발전 속도도 인간의 통제 능력에 맞춰 늦춰질 수 있다고 주장합니다.