수십 년 걸린 '유한 단순군 분류' 증명, Lean으로 완전 형식화되다
Classification of Finite Simple Groups Formalized in Lean
유한 단순군 분류는 약 100명의 수학자가 수십 년에 걸쳐 수천 페이지 분량으로 완성한 집단적 성과다. 이제 이 1세대 증명 전체를 Lean으로 형식화해 모든 논리 단계를 커널이 검증했다. 4,310만 줄의 Lean 코드와 205만 개 선언, 715편의 문헌이 동원됐으며, 과정에서 기존에 발표된 '불균형 군 정리' 증명의 오류를 발견해 대안 경로를 제시했다.
그 과정에서 우리는 발표된 불균형 군 정리(Unbalanced Group Theorem) 증명의 문제점을 발견했다.
HN 토론
48- sleepyams
어찌 보면 유한 단순군의 분류는 수학자로서 나를 불안하게 만드는데, 아마 이게 그 불안감을 잠재우는 데 도움이 될 것 같다.
- mlmonkey
궁금해서 묻는데: 최전선 모델을 가져다가 세상의 모든 수학 교과서에 풀어놓고, 모든 증명/정리/보조정리 등을 Lean으로 변환하는 게 가능할까? 최전선 모델이라면 그렇게 할 수 있지 않을까? 그리고 이건 일회성 작업이다: 한 번 해두면 영원히 거기에 있고, 다른 증명에 사용할 수 있는 라이브러리로 제공된다.
어쩌면 내가 Lean을 잘못 이해하고 있는지도 모르겠다. 나는 Lean을 수학을 위한 프로그래밍 언어라고 생각하고 있다.
- sebzim4500
이건 자동 형식화의 아주 좋은 활용 사례인 것 같다. 왜냐하면 과거에 수학자들이 분류를 끝냈다고 잘못 믿었다가 빠진 클래스/산재군을 발견한 적이 있기 때문이다.
원래 증명은 약 100명의 수학자가 협력한 결과였는데, Tao가 맞다면 앞으로 물리학에서처럼 더 많은 이런 협업을 보게 될 것이다.
- compacct27
군은 내가 추상대수학에 빠져들게 한 관문이었다. 한 친구가 대칭이 어디에나 있으며 군이 대칭을 형식화하는 방법이라고 알려줬고, 그 모든 것을 이해하는 것은 미친 여정이었다. 최전선 모델은 그 추상적인 개념들을 평범한 영어 예시와 연결하고 질문에 꽤 잘 답할 수 있다. 혼자서 이 분야를 시작하고 그것이 우리에게 무엇을 제공하는지 보기에 더 좋은 때는 없었다.
- senderista
이런 잘 알려진 공백을 메우는 것은 AI 회사들이 해야 할 일이지, 진행 중인 연구를 가로채려는 것이 아니다.