유한 단순군 분류 정리, Lean으로 완전 형식화: 4,310만 줄에 선언 205만 개

Lean으로 4,310만 줄이라니. 역대 가장 긴 Lean 증명인 건 확실한데, 이게 수학적으로 쓸모가 있는지는 잘 모르겠음.

이런 작업에 자동 형식화를 쓰는 건 좋은 선택인 듯. 예전에 분류 정리가 끝났다고 믿었다가 나중에 뒤집힌 적도 있잖아.

빠진 산재군이 나온 게 아니라 quasithin case 문제임. 600쪽짜리 미발간 원고에 들어 있던 부분인데 나중에 불완전한 걸로 드러난 거더라.

프런티어 모델을 모든 수학 교과서에 풀어놓으면 전부 Lean으로 바꿀 수 있지 않을까? 한 번만 해두면 영원히 라이브러리로 남는 거잖아.

기본적인 정리도 정리하는 방식이 워낙 많아서 어떤 걸 라이브러리에 넣을지는 사람이 정해야 함. 두세 개 넣는다고 해도 모든 형태를 다 담을 수는 없음.

우리가 한 게 딱 그거임. 500편 넘는 논문과 책을 에이전트 떼로 훑었는데, 같은 개념을 소스마다 조금씩 다르게 형식화해서 하나로 합치는 게 제일 힘들었음.

페이지가 뒤로가기 버튼을 가로채는 버그가 있음. 새 탭에서 여는 걸 추천.

LLM이 한 형식화는 사람이 한 것만 못하지만, 분류 정리가 맞다는 게 확인된 것만으로도 좋음.

구멍을 하나만 찾았다는 게 의외임. 논문 수십 편에 흩어진 결과면 고칠 만한 데가 여럿 나올 줄 알았는데.

지난 40년 동안 사람들이 이미 많이 찾아서 메꿔놨음. 이번에 새로 생긴 구멍은 아니지.

블로그를 보면 출판된 기록에서 중요하게 다른 지점이 34곳 있었고, 그중 제일 큰 게 Unbalanced Group Theorem이라고 적혀 있더라.

AI 회사들이 진행 중인 연구를 가로채는 대신 이런 잘 알려진 구멍 메우는 일을 해야 함.

호모토피 기반 사람들이 결국 못 뭉친 게 아쉬움. 형식화는 이렇게 성숙했는데 여전히 집합론 기반 라이브러리가 표준임.

조금씩 나아지는 중임. cubical 쪽 라이브러리 작업도 돌아가고 있음.

Lean은 집합론이 아니라 타입 이론이니까 HoTT로 옮기는 건 생각보다 쉬움.

지난주에 Claude Max 주간 예산을 다 써서 Mathlib를 Coq-HoTT로 옮겼는데 결과물이 너무 예뻐서 이번 주에도 또 할 예정임.