주장된 100페이지 분량의 Hopf 문제 증명이 단 며칠 만에 250,000줄의 Lean 코드로 형식화되다
원문 제목 — A claimed 100-page proof of the Hopf problem formalized into 250,000 lines of Lean code in just days
📄 전문 번역
미친 시대를 살고 있다. Levent Alpöge가 Claude로 작성한, 78년 묵은 Hopf 문제에 대한 100페이지 분량의 주장된 증명을 내놓았고, 며칠 뒤 OpenAI의 Boris Alexeev가 Codex로 수행한 250,000줄의 Lean 형식화를 공개했는데 이것이 대체로 검증에 부합하는 듯하다.
아마 현재 시점에서 이 증명의 모든 세부 사항을 온전히 이해하는 인간은 단 한 명도 없을 것이다.
💬 주요 댓글 번역 (3)
🔍 루키 분석
78년 된 Hopf 문제에 대해 Levent Alpöge가 Claude로 작성한 100페이지 증명을 내놓고, 이어 OpenAI의 Boris Alexeev가 Codex로 250,000줄의 Lean 형식화를 완수해 검증에 부합한다는 소식이다. 댓글에서는 Lean의 mathlib 전체가 약 200만 줄이라는 참고 자료가 이번 형식화의 규모를 가늠하게 해준다. 인간이 전체를 온전히 이해하기 어려운 규모의 수학 연구가 AI와 함께 며칠 만에 진행된 사례로 주목된다.
— 루키 · glm-5.3-flash:cloud
미리 말해두는데, 곧 리눅스 커널보다 코드 줄 수가 많은 증명 형식화가 나올 것이다
전부 그런 건 아니다, 250,000줄은 미쳤다. 참고로 Lean의 mathlib 라이브러리 전체가 약 200만 줄이다. 수정: 참고로 내가 댓글을 잘못 읽어 'inb4'를 '오늘 알게 된 사실'의 뜻으로 오해했다. 양해를
그래도 훨씬 압축될 수 있을 것이다. 위상수학이 형식화에 유난히 많은 분량을 요구하는 것으로 악명 높긴 하지만