검증 기다려봐야 하는거 아니냐는데

수학 증명은 원래는 논문 형식으로 발표 후 검증하고 한참 뒤에 Lean 증명으로 정리되는데

이번 해결책은 이미 처음부터 Lean 증명 형태로 내놓아서 걍 게임 끝이라는 분위기임

(Lean 증명이란, 수학 증명과정을 마치 코딩처럼 컴퓨터가 돌려볼 수 있게 정리하는 형태로, 이게 맞으면 그냥 100% 맞다고 보면 됨, 계산기 사칙연산이 틀릴리가 없듯이)

현재 오픈AI가 공개한 repo는 Lean 4에서 빌드하도록 되어 있고, 누구나 독립적으로 certificate를 다시 검사할 수 있게 올려놨는데 이미 오류가 없음

이 중에 3번 나비에-스토크스 방정식을 이번에 GPT가 푼거고, 나머지도 곧 풀겠다고 함