어제, 오늘자 테렌스 타오가 업로드한 게시물들



7ef3c028e2f206a26d81f6ed4f80706a




GPT-5 Pro 바이브 코딩으로 수학 증명 시도 사례



"... 이 과정은 이틀에 걸쳐 진행되었지만, 제 실제 집중 시간은 처음부터 끝까지 두세 시간 정도밖에 필요하지 않았습니다.


제가 이 명제를 (더 전통적인 검색 도구와 깃허브 코파일럿의 자동 완성을 사용하되, 최신 AI는 사용하지 않고) 직접 형식화하는 대조 실험을 하지는 않았지만,

대략 6시간 정도 걸렸을 것이라고 추정합니다.

(아마 그렇게 했다면 증명이 훨씬 더 우아했을 겁니다.)


"vibe-coded" 증명은 1125줄에 달하며, 그중 상당수는 grind와 같은 강력한 린(Lean) 택틱으로 이미 증명 가능한 매우 자명한 것들을 증명하는 데 할애되었습니다.


하지만 이 결과는 인간의 증명이 불분명하거나 설득력이 없었던 경우는 아니었고, 저는 이 실험을 통해 린(Lean) 형식화 경험을 추가로 얻을 수 있었습니다.



요약하자면, 이러한 종류의 도구들은 린(Lean) 타입체크와 같은 엄격한 검증 방법과 결합될 때,

단계별로 실행될 경우 시간이 많이 걸리는 연구 수준의 여러 작업들을 (평균적으로) 어느 정도 가속화하는 수준에 도달하고 있다고 생각합니다.


다만, 여전히 예측 불가능한 성능 편차와 통합 워크플로우의 장벽이 존재하여 과정이 완전히 매끄럽지는 않으며,

사용 가능한 결과물을 내놓지 못하는 적지 않은 쿼리들을 제대로 수정하기 위해서는 해당 작업에 대한 충분한 전문 지식이 필요합니다."



-> GPT-5 Pro로 vibe coding하여 수학 연구 수준 증명 작업 시도시,

직접 한 것만큼 깔끔하진 않지만 타오가 직접 했다면 6시간 정도 걸렸을 일을 2-3시간만 집중하여 가능하도록 함.


이에 대해 현재 LLM들이 어느 정도 리서치 수준의 작업들을 가속화하는 수준에 도달하고 있다고 평가함.






Terence Tao (@tao@mathstodon.xyz)

The process was spread out over two days, but I think only about two or three hours of my actual attention was required from start to finish. I did not attempt a control experiment to formalize the same statement by hand (using more conventional search tools and Github Copilot's autocomplete, but not frontier level AI), but I roughly estimate it would have taken perhaps six hours to do so. Most likely the proof would be much more elegant: the

mathstodon.xyz

https://mathstodon.xyz/@tao/115493672527637142