OpenAI는 내부 프런티어 모델이 수백 건의 수학적 성과를 냈다고 밝혔습니다. 여기에는 Lean으로 형식화한 증명과 미해결 연구 문제를 다룬 독창적인 작업이 포함됩니다. 새로움은 두 가지입니다. 후보 결과의 규모가 크다는 점, 그리고 대화형 증명 보조기를 사용해 형식화함으로써 자연어 논증에 그치지 않고 검증 가능한 산출물을 만들었다는 점입니다. 생성형 추론과 기계 검사형 출력의 결합은 초기 모델 아이디어를 기계적으로 검증할 수 있는 결과물로 이어 주는 경로를 제공한다는 점에서 차별화됩니다. 덕분에 텍스트로만 제시된 주장보다 독립적인 재현도 빨라질 수 있습니다.

그동안 프런티어 모델은 주로 코딩 능력과 언어 과제를 기준으로 평가되어 왔습니다. 독창적인 수학적 내용을 만들어 내는 것은 창의성과 과학의 영역으로 한 걸음 들어서는 일입니다. 수학적 발견에는 새로운 추측을 제시하고, 만만치 않은 논증을 구성하며, 기존 결과를 종합해 지식을 진전시키는 일이 필요합니다. 모델이 새로운 보조정리를 찾아내거나 복잡한 증명의 빈틈을 메울 때, 개발자용 도구보다 연구 보조자에 가까운 역할을 수행합니다. 이에 따라 모델의 결과물을 활용하는 주체와 방식도 달라집니다. 프로그래머의 구현 속도를 높이는 데서 연구자의 가설 생성과 증명 구성을 가속하는 방향으로 바뀌는 것입니다.

Lean을 통한 형식화는 모호성을 줄여 주지만 검증 작업을 없애 주지는 않습니다. 비형식적인 모델의 제안을 완전히 명세된 Lean 증명으로 옮기려면 정의를 선택하고 보조정리를 인코딩하며 증명 스크립트를 조정하는 등 사람의 엔지니어링 작업이 필요한 경우가 많습니다. Lean 형식화는 의존 관계와 숨은 가정을 드러내지만 그 과정에서 자체적인 오류가 생길 수도 있습니다. 따라서 견고한 절차에는 자동 증명 검사, 정확한 환경과 도구 체인 버전을 갖춘 재현 가능한 저장소, 그리고 모델의 주장이 최초 산출물에만 의존하지 않는지 확인하는 독립적인 전문가 재현이 함께 필요합니다.

AI가 생성한 수학적 결과는 기관이 저자 표기와 공로 인정 관행을 재검토하도록 요구합니다. 모델의 도움을 크게 받아 발견한 정리라면 인간 연구책임자, 모델 개발자, 양쪽 모두, 아니면 어느 쪽도 저자로 표기하지 않아야 할까요? 이와 함께 출처 기록도 중요합니다. 버전이 관리된 증명 스크립트와 모델 체크포인트, 초기 프롬프트, 사람의 수정 내역을 기록해야 검토자가 아이디어의 발전 과정을 추적할 수 있습니다. 학술지와 학회는 모델 사용 사실을 명시하도록 투고 규정을 갱신하고, 출처 기록이 불완전할 때 AI가 도출한 주장을 어떻게 인정하거나 배제할지 기준을 마련해야 합니다.

팀은 구체적인 실천 방안을 마련해야 합니다. (1) 모델 출력을 형식화와 독립 검증이 필요한 초안 산출물로 다룹니다. (2) 증명 스크립트를 버전 관리하고 사용한 모델과 프롬프트를 정확히 기록합니다. (3) 도메인 전문가와 검증 엔지니어가 함께하는 학제 간 검토 절차를 만듭니다. (4) 환경 정보 수집과 증명 재실행을 자동화하는 도구에 투자합니다. 연구 지원 기관은 모델 규모나 벤치마크에만 집중하기보다 검증 격차를 줄이고, 재현 가능한 기계 보조 수학을 가능하게 하는 커뮤니티 기반 시설을 뒷받침하는 프로젝트를 우선해야 합니다.