Anthropic이 유명한 수학 난제를 증명한 것으로 보이지만, 연구자들은 여전히 '왜' 그런지 이해하려고 노력 중이다🤔
Anthropic appears to have proved a famous mathematical conjecture, but researchers are still trying to understand WHY?🤔
핵심 요약
Anthropic의 AI가 수학 난제를 증명했으나, 인간이 그 논리를 이해하고 검증하는 과정이 과제로 남았습니다.
- 수학 난제 해결 — Anthropic의 AI가 Lean을 활용해 유명한 퍼콜레이션 난제를 증명함
- 의미론적 압축 해제 — 수학자들이 AI가 도출한 증명 과정을 인간이 이해할 수 있는 형태로 해석 중임
- 인간-AI 협업 — AI가 방대한 증명 공간을 탐색하고 인간이 개념적 돌파구를 마련하는 협업 모델이 주목받음
- 증명 정의 논쟁 — AI의 증명을 인간이 이해하지 못해도 증명으로 인정할 수 있는지에 대한 의견이 갈림
8월 28일, 고정된 GitHub commit에 올라온 Anthropic의 아티팩트는 유명한 퍼콜레이션 추측(percolation conjecture)을 겨냥해서 Claude가 직접 짠 Lean 코드를 담고 있어.
공교롭게도 필즈상 수상자인 위고 뒤미닐코팽(Hugo Duminil-Copin)이 8월 30일에 딱 이 상황을 예견하는 에세이를 썼더라고. AI만이 이 문제를 풀 수 있을지도 모른다는 우려 섞인 내용이었지.
그 양반도 수년 동안 이 문제 붙잡고 씨름했는데, 인간보다 AI가 먼저 풀어낼 것 같다고 적어놨더라. 물론 본인이 시도했던 방식들은 비록 실패했지만, 그 과정에서 나온 아이디어들이 나중에 다른 수학적 성과로 이어지긴 했다고 해.
근데 진짜 소름 돋는 지점은 이거야:
인간이 '왜' 참인지 이해하기도 전에, 기계는 이미 그게 '참'이라는 걸 알아버릴 수도 있다는 거지.
Lean은 형식적으로 정의된 엄청나게 긴 연역 과정을 검증할 수 있어. 정의, 정리의 명제, 의존성, 그리고 커널만 제대로 되어 있다면 이런 결과를 얻을 수 있거든. "정리 증명 완료✓"
물론 인간이 머릿속으로 그리는 "아! 당연하네. 그래서 이게 되는 거였구나" 같은 직관적인 모델은 아직 없는 상태로 말이야.
지금 수학자들이 하는 짓이 딱 그거야. 그 기계가 뱉어낸 결과물을 인간이 이해할 수 있게 풀어내는 '의미론적 압축 해제'를 하고 있는 거지.
