저는 GPT-Astra를 수학 문제에 직접 테스트해봤습니다. 말 그대로 퀀텀 점프(quantum leap) 수준의 도약입니다.
모델과 대화를 주고받으면서 동시에 Lean으로 명제를 실시간 증명할 수 있습니다. 그 느낌은 정말 놀랍습니다. 자신의 아이디어를 즉시 검증하고, 말 그대로 ‘진실을 컴파일(compile truth)’할 수 있습니다.
수학자의 입장에서 보면, 이제 드디어 아이디어를 떠올리고 탐구하는 데 거의 전적으로 집중할 수 있는 시대에 들어선 것처럼 느껴집니다. 논리의 큰 틀이 잡히기만 하면 각각의 보조정리(lemma)가 자연스럽게 이어집니다.
예전에는 아이디어를 떠올린 뒤 실제로 그것을 형식적으로 검증하는 작업이 한참 뒤따라와야 했습니다. 하지만 Astra는 매우 빠릅니다. 많은 경우에는 Codex에서 논증을 써 내려가는 동시에 형식화가 거의 실시간으로 함께 이루어집니다.
모델에게 리터러리 프로그래밍(literate programming)과 LaTeX를 함께 사용하라고 지시하면, 사람이 읽는 수학적 증명과 Lean 코드가 하나로 결합된 형태의 결과물을 얻을 수 있습니다. 자신이 작성한 설명이 그대로 유지되면서, 그 사이사이에 이해하기 쉬운 짧은 Lean 코드 조각들이 들어갑니다.
저는 이제 증명의 유일한 확인 방법이 단지 “아하, 맞는 것 같아”였던 시대로 돌아가고 싶지 않습니다.
이제는 그 “아하!”라는 직관적 깨달음 뒤에 초록색 체크 표시가 따라옵니다. 그리고 그것은 내가 정말로 그 아이디어의 본질을 정확하게 포착했다는 사실을 확인해 줍니다.
상상해보세요. 언젠가 세상의 모든 보조정리들이 하나의 거대한 데이터베이스에 연결되고, 각각의 정리가 그것을 발견한 사람이나 모델과 연결되어 있는 모습을 말입니다.
우리는 그 안에서 서로 다른 아이디어를 조합하고 섞으면서, 거인들의 어깨 위에 올라서서 새로운 것을 만들어갈 수 있습니다.
다만 이제는 훨씬 더 멀리 볼 수 있고, 훨씬 더 빠르게 쌓아 올릴 수 있습니다.
그리고 우리는 아직 이런 변화의 아주 초입에 있을 뿐입니다.
해야 할 일은 정말 많고, 그만큼 재미있는 일도 엄청나게 많습니다.
https://x.com/nasqret/status/2095620909583274335