아니 12일만에 d=3부터 d=5까지 다 풀어버렸네... Knuth 교수가 괴롭혔던 홀수 주기 문제가 Claude한테 하루만에 끝나더니, Lean 4 포말라이제이션까지 5일만에 끝낸 거 실화냐
d=4 증명하고 바로 d=5로 넘어가서 짝수 추상화하는데 이제 짝수도 거의 다 풀렸다는데?? 게다가 합성수는 소수만 증명하면 자동으로 풀린다는 사실까지 증명함
GPT 5.4 프로, Opus 4.6, 제미니 딥씽크 이 조합 실제로 저런 난제를 씹어먹네... 개추 대신 진짜 GPT에다가 이 문제 던져보라니까 개웃기다 ㅋㅋ 저런 속도면 내년엔 수학계 판도 완전히 바뀔듯
이 글 아래에서 이어진 반응을 시간순으로 읽을 수 있습니다. 총 2개
Knuth 문제가 트럭에 실리는 뉴스라지만 진짜 핵심은 Lean 4 포말라이제이션 단계야. 모델이 d 값을 늘릴 때마다 '증명이 되었다' 식으로 주장하는 부분이 아니라, 실제 Coq/Lean 레벨에서 증명 검증이 1초도 안 걸리는 절차적 속도가 중요한 거지. d=5 가 증명 완료라고 해도 나중에 저걸 컴파일러가 증명했음 이라고 띄울 때 오류가 터지면 다 날아가는 거거든? 지금 AI 팀이 만든 건 단계별 증명이 아니라 프롬프트 기반 추론 스택이라, 다시 재현하면 결과가 달라질 수도 있어.
Knuth 문제를 하루만에 풀었다니 놀라운 건 맞는데, 여기서 가장 무서운 건 증명 과정이 사람 손을 안 타고 있다는 거야. d=4에서 d=5로 넘어가는 순간 레빗 홀 문제가 생길 수 있는데, 모델이 이걸 인지 안 한 채 짝수 추상화로 넘어가버리면 오류 쌓이는 게 뻔하지. 짝수가 거의 다 풀렸다고 하는데 '거의'가 정확히 어디까지인지 모르겠고, 합성수가 소수 증명으로 자동 해결된다는 주장도 수치 해석 범위를 넘어서면 틀어질 가능성 있잖아. 이 속도로 12일만에 3단계나 확장하면 다른 수학자들이 오류 잡기도 전에 그냥 넘어가버리는 경우 생길 수도 있어서 오히려 연구 품질이 떨어질 수 있다는 거.
