OpenAI, 수학 결과 3건 철회하고 Lean 형식화 현황 공개함

증명도 소프트웨어처럼 출시되는 시대라는 댓글 봤는데, 그럼 릴리스 전 검증은 누가 함?

철회 목록이 Weil 클래스, Kuga-Satake, K3 곱 표면 세 개인데 원래 확인 없이 올린 거 아니냐는 얘기가 많음.

철회 전에 왜 확인 안 하고 올렸냐는 말에 공감함. 발표하고 나중에 고치는 순서가 이상함.

초기 글들 읽어보면 slop 느낌이 강하고 덜 다듬어진 게 티 남. 내부에서 결과 검증할 사람이 적은 거 아닐까 싶음.

반대로 사람들을 일찍 끌어들이고 투명하게 공개하려는 게 원래 목적 아님?

Lean으로 검증됐다고 해도 정의가 맞는지가 문제임. 형식화가 살짝 다른 문제를 푸는 걸 수도 있음.

블로그 원문 보면 검증 전에 먼저 공개하고 나중에 Lean 증명 추가하겠다고 했더라. 42% 중 일부는 검증되고 일부는 틀린 거 같음.

2천만 줄짜리 Lean 증명이면 수학이 아니라 Lean solver를 퍼징한 거 아닐까 의심됨.

페르마 정리 증명도 큰 결함이 있어서 2년 걸려 고쳤음. 사람 증명도 완벽하진 않음.

IPO 앞두고 PR로 올린 거라는 의심은 있는데, IPO가 내년이라 시기가 좀 안 맞더라.

행렬 곱 상한 결과는 이론상 빠른 갈락틱 알고리즘이라 실제 크기에서는 거의 의미 없음. 이전 최고치 2.371177보다 조금 나은 정도임.