AI·바이브코딩 기술 트렌드

팔로마: AI가 쏟아내는 Lean 증명을 검증하는 등록소가 열렸다

최근 몇 달 사이 오래된 난제부터 새로운 결과까지 인공지능이 만들어낸 수학 증명이 눈에 띄게 늘었고, 그중 일부는 증명 보조 언어인 Lean으로 형식화되기도 했다. 문제는 특정 Lean 저장소가 정말로 주장하는 명제를 증명하는지 확인하는 일이 결코 간단하지 않다는 점이다. Lean에 익숙하지 않은 독자라면 더욱 그렇다. 우선 형식화된 Lean 명제에 딸린 ...