HN
Hacker News • 15일 전
IMP 8
OpenAI 나비에-스토크스 증명, Lean 4 형식 증명 동시 공개
OpenAI가 유체역학의 나비에-스토크스 방정식 관련 오랜 난제를 해결한 증명을 발표하며, 기존의 사람이 읽는 증명과 함께 기계 검증이 가능한 Lean 4 형식 증명도 함께 공개했습니다. 과거 학부 교과서 한 페이지를 형식화하는 데 약 40시간이 걸리던 것과 비교하면, OpenAI가 166페이지 논문의 증명을 17시간 만에 검증한 것은 비용을 4자리수(만 배) 수준으로 줄인 혁명적 변화입니다. 형식 검증은 수학뿐 아니라 보안 정책, 스마트 컨트랙트, 미션 크리티컬 알고리즘 검증에도 적용될 수 있습니다.
형식 증명 Lean 4 나비에-스토크스