Palomar: Lean 검증 수학의 등록소

Palomar: A registry of Lean verified mathematics

최근 AI가 생성한 수학 증명이 쏟아지면서, 실제로 Lean으로 검증되었는지 확인하기 어려워졌습니다. 이를 해결하기 위해 Lean FRO와 ICARM이 주도하는 Palomar 레지스트리가 출범했습니다. Palomar는 GitHub 저장소의 스냅샷을 등록받아, 증명이 타입체크를 통과하고, 추가 공리 없이 정확히 주장된 결과를 증명하는지, 그리고 비공식 설명과 일치하는지 확인합니다. 첫 번째 검사는 기계적으로, 두 번째는 대규모 언어 모델로 수행됩니다. Terence Tao는 Sendov 추측의 형식화를 성공적으로 등록했으며, 인간 생성 및 AI 생성 증명 모두 환영합니다.