AI 시대 수학자 평가에 문제 선택과 증명 이해를 반영하자는 칼레가리
시카고대 수학 교수 프랭크 칼레가리는 OpenAI의 2026년 10월 수학 결과 공개를 계기로, 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 증명과 논문 설명의 차이, 모델의 추론 경로를 확인하기 어려운 점은 남아 있습니다.
Julia로 배우는 미적분
Julia를 활용해 미적분을 배우는 온라인 노트입니다. 수치 계산과 그래프를 중심으로 개념을 설명하고, 연습 문제와 자기 채점 답안도 제공합니다.
테렌스 타오의 ‘수학 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에서는 수학의 개방성과 인간의 이해를 지킬 방안을 두고 찬반이 맞섰습니다.
Factorio 품질 생산 계산하기
Factorio: Space Age의 품질 생산과 재활용 과정을 행렬과 선형 방정식으로 모델링하고, 장기 생산량을 정확히 계산하는 방법을 설명합니다. 저자는 계산을 자동화한 웹 도구와 소스 코드도 공개했습니다.
Forisek–Jancina 방식으로 32비트 정수를 빠르게 소수 판정하기
Forisek와 Jancina가 제안한 결정론적 소수 판정법은 32비트 정수에서 소수 2, 3, 5, 7로 나누어 확인한 뒤 해시로 밑을 고르고 강한 probable-prime 검사를 수행합니다. 밑을 담은 조회 테이블은 512바이트만 차지하며, 글에는 C 구현이 실려 있습니다.