Lean 4.35.0부터 검증된 커널 4개를 함께 배포, con-leche는 일관성까지 증명됨
- lake check 명령이 추가되어 leanchecker로 개발 결과를 다시 검증하고, 실행은 기본적으로 샌드박스 안에서 이뤄짐
- Lean이 nanoda, lean4lean, con-leche, con-ron 등 외부 커널 4개를 함께 배포하고 lake check --paranoid로 전부 돌리게 함, 메모리 손상은 조용한 오답 대신 검사된 중단으로 바뀜
- con-leche는 Lean으로 작성되고 일관성이 증명된 첫 커널임, Mathlib 전체를 8 스레드로 약 100초에 검사하며 공식 커널 대비 명령어 수는 0.69배임
- con-ron은 Joachim Breitner가 AI로 con-leche를 Rust로 옮기고 Aeneas로 정제 관계를 증명한 커널임, 컴파일러나 런타임 버그를 줄이려는 목적임
- FLT 13M LoC, Mathlib 2.5M LoC, 50M LoC를 넘는 저장소까지 등장해 현재 외부 커널 방식으로는 확장이 어려워서 증분 검사와 바이너리 내보내기 형식이 필요함
Hacker News 의견들
잘 모르겠는데 이거 검사기 위에 검사기 얹는 구조 아님? 근데 핵심은 커널마다 같은 버그를 가질 가능성이 낮다는 거임. 커널 여러 개로 돌리면 증명 틀릴 확률이 확 줄어드는 거지.
15년 전에 지금 Lean이 있었으면 올해 수학 난제들 얼마나 풀렸을까? 그게 LLM 덕인지 Lean 자체가 좋아서인지 궁금함.
나도 같은 생각임. LLM 매일 쓰는데 초인적인 지능은 못 봤음. 수학이 프로그래밍으로 번역되면서 난독화가 벗겨진 거라고 봄.
수학 대학원 때 Lean으로 자명한 보조정리 몇 주씩 붙잡고 있었음. 이건 새 수학 찾는 툴이 아니라 형식화 툴임. LLM이 창의성 내고 Lean 타입체커가 틀린 거 잡는 루프가 핵심임.
Coq도 오래전부터 있었잖음.
Mathlib PR이 Opus 4.6 나왔을 때 확 튀었음. 큰 형식화 프로젝트들은 LLM 없었으면 여기까지 못 왔을 거임.
Absolutely none 같음. 자연어 증명 없이 형식 증명부터 쓰는 사람은 못 봤음. 감 없이 전술만 던지면 사소한 증명 말고는 진척이 거의 없음.
공개키 인증서 만료 설명하다가 삼촌이 멍해졌던 얘기처럼, 수학도 용어 장벽만 넘으면 생각보다 단순한 거 아닐까 싶음.