OpenAI, 나비에-스토크스 166쪽 증명과 Lean 4 형식 증명 함께 공개

형식화 비용이 크게 줄었다는 얘기는 AI가 증명을 실제로 만들었다는 얘기보다도 더 오래전부터 나왔음. 이번 발표가 그 흐름을 더 널리 알린 정도라고 봄.

에이전트 비용이 약 $40M이었다는 추산도 있더라. 글의 기준으로 인간 작업을 환산하면 약 88만 시간, 시간당 $150이면 $132M쯤이라 4자릿수 격차라고 하긴 어렵고, 100만 시간 지식노동을 조율하는 비교도 현실적이지 않음.

2005년의 페이지당 40시간 규칙은 증명 자동화가 약했던 시절 산물임. Lean 쪽은 수학자가 쓰기 편하도록 자동화에 오래 투자해서 지금 수치로 그대로 잡기 어렵다고 봄.

그럼 학부 수학 한 페이지를 지금 형식화하는 데 몇 시간이 든다고 보나? Mathlib이 학부 수학을 충분히 덮으면 거의 0에 가까워진다는 뜻인지 궁금함.

이번 발표에서 정작 결과 자체보다 다른 얘기만 하는 사람이 많음. 범용 프로그램이 이런 규모의 문제를 풀었다는 사실 자체가 엄청난데, 직접 증명이나 귀납 증명도 해낼지 보고 싶음.

실제 수학자가 AI로 작업한 노트가 다음 세대 학습 데이터에 들어간 뒤 모델이 가져온 것일 수도 있음. 그 가능성은 확인해야 함.

대부분은 나비에-스토크스보다 자기 프롬프트의 학습 제외가 작동하는지에 더 익숙하니까, 자기 생활에 바로 닿는 쪽을 말하는 거겠지.

다른 연구자의 산문 메모에서 영감을 얻었거나 직접 접근했다 해도, 전 범위를 Lean 프로그램으로 빠르게 옮겨 기계 검증까지 통과했다면 그 자체로 대단한 결과임.

수학 학사 학위가 있어도 인간 증명이나 LLM 증명을 이해하려면 엄청난 시간과 노력이 들 것 같음.

계산 비용만 약 $10M이라는 추산도 봤음. 그 돈이면 연구자 20명에서 25명을 5년 고용할 수 있으니, 지금 최첨단 접근은 돈 많은 곳만 가능한 수준임.

지금도 결과 대신 LLM과 컴퓨터의 일반 능력을 말하고 있잖아. 다른 사람들을 비판하면서 똑같은 화제로 건너뛰는 셈임.

문제의 중요한 단계를 다른 연구자 작업에서 베낀 것이라면 모델이 실제로 얼마나 새 아이디어를 냈는지 알 수 없음. 표절 의혹이 정리되기 전에는 성과의 의미를 판단하기 어렵다고 봄.

2005년보다 Lean 형식화가 쉬워진 건 맞고, Mathlib이 공리와 보조정리를 많이 제공함. 그래도 공개된 코드는 유체역학 개념이 백과사전처럼 들어간 수준이라 이 정도 알고리즘을 Lean으로 형식화한 일은 대단함.

Lean 검증은 느린 편인 듯함. 페르마의 마지막 정리는 230GB 메모리에서 검증 15시간, 에이전트 코드 생성은 11일이었다는데, 감사 가능성을 지키면서 얼마나 최적화할 수 있을지 궁금함.

그 비교는 하드웨어와 병렬성부터 맞춰야 함. 에이전트는 큰 추론 클러스터에서 병렬로 돌고 Lean 검증은 단일 장비일 가능성이 높으며, 에이전트도 내부에서 검증기를 수없이 돌렸을 것임.

인스타그램에서 들은 얘기라 신뢰도는 낮지만, 가장 근접했던 교수가 몇 주 전 Codex에 자기 노트를 넣었다는 소문이 있음. 사실이면 우연치고는 묘한데, 학습 실행은 수개월 걸리니 이전 학습에 들어갔을 가능성은 낮아 보임.