AI가 참여한 11개 정사각형 최적 포장 증명, Lean 형식 검증 완료
2026년 10월 6일 공개된 GitHub 저장소에서 OpenAI의 Astra와 Anthropic의 Claude가 기여한 11개 정사각형 포장 최적성 증명이 Lean으로 완전 검증되었습니다.
JORE2
Lean
왜 하필 Lean 일까? 증명 도구의 독점과 그 이면의 역사
수학 형식화 분야에서 Lean 이 사실상 표준처럼 여겨지면서, 왜 다른 도구를 쓰지 않는가에 대한 질문이 뜨겁습니다. 60 년의 역사를 가진 AUTOMATH 부터 Isabelle, Coq 에 이르기까지 다양한 경쟁자들이 존재…