AI 생성 이미지
AI-assisted proofs의 핵심은 “AI가 혼자 증명을 완성한다”가 아닙니다. 더 중요한 변화는 수학 연구의 작업 방식입니다. 전문 수학자가 문제의 방향과 엄밀성 기준을 잡고, AI가 아이디어 실험·문헌 탐색·계산 탐색·부분 증명을 빠르게 시도하는 협업 구조가 현실적인 모델로 떠오르고 있습니다.
이 변화는 단순히 더 똑똑한 채팅봇을 쓰는 문제가 아닙니다. 수학 연구처럼 오래 이어지는 작업에는 가설을 세우고, 실패한 접근을 기록하고, 정의를 수정하고, 다시 검증하는 과정이 필요합니다. AI-assisted proofs를 이해하려면 “정답 생성”보다 “연구 흐름을 어떻게 관리하고 검증하는가”를 봐야 합니다.
채팅봇이 아니라 상태를 가진 연구 작업대
Google의 AI co-mathematician은 수학자가 AI 에이전트와 함께 개방형 연구를 수행하도록 설계된 워크벤치입니다. 아이디어 발상, 문헌 검색, 계산 탐색, 정리 증명, 이론 구축을 지원하도록 최적화됐습니다.1
핵심 차이는 상태 유지입니다. 일반 채팅 인터페이스는 질문과 답변이 끊어지기 쉽고, 장기적인 연구 맥락을 안정적으로 관리하는 데 한계가 있습니다. 반면 AI co-mathematician은 며칠 또는 몇 주에 걸쳐 이어지는 가설, 실패한 시도, 사용자 의도, 수학적 산출물을 작업공간 안에서 추적하도록 설계됐습니다.1
이 구조는 주니어 연구자와의 협업에 가깝습니다. AI는 여러 접근을 병렬로 시험하고, 계산이나 문헌 탐색을 수행하며, 유망한 중간 결과를 제시합니다. 전문 수학자는 그중 의미 있는 방향을 고르고, 숨은 가정이 없는지 확인하며, 증명의 엄밀성을 판단합니다.
달라지는 것은 속도보다 연구 분업이다
AI co-mathematician은 프로젝트 조정자 에이전트가 복잡한 문제를 여러 병렬 작업흐름에 위임하는 구조를 사용합니다.1 이는 수학 연구를 하나의 질문에 대한 즉답으로 보지 않는다는 점에서 중요합니다. 실제 연구는 단번에 끝나는 풀이가 아니라, 가설을 만들고 반례를 찾고 정의를 다듬는 반복 과정에 가깝습니다.
따라서 AI-assisted proofs의 가치는 “한 번에 완벽한 증명을 쓰는 능력”에만 있지 않습니다. 더 실용적인 가치는 다음과 같습니다.
가능한 접근법을 빠르게 넓혀 본다.
실패한 가설을 기록해 같은 실수를 줄인다.
계산 탐색과 문헌 탐색을 병행한다.
부분 증명이나 보조정리를 후보로 제안한다.
인간 연구자가 검토할 수 있는 중간 산출물을 만든다.
이때 수학자의 역할은 줄어들기보다 바뀝니다. 모든 탐색을 직접 수행하는 대신, 문제를 잘 쪼개고, 좋은 중간 목표를 세우고, 결과의 의미와 엄밀성을 판정하는 일이 더 중요해집니다.
증명의 병목은 생성보다 검증이다
AI가 그럴듯한 자연어 증명을 내놓는 것과, 실제로 맞는 증명을 만든 것은 다릅니다. 수학에서는 작은 생략, 암묵적 가정, 정의의 미세한 오해가 전체 증명을 무너뜨릴 수 있습니다.
그래서 Lean 같은 proof assistant가 중요해집니다. ProofBench는 자연어 문제와 Lean 4 형식 명제를 주고, 모델이 기계가 검증할 수 있는 증명을 작성하는지 평가합니다.2 이 방식은 “그럴듯한 설명”이 아니라 실제로 컴파일되는 논리만 통과시킵니다.
다만 아직 격차는 남아 있습니다. ProofBench에서 전문 시스템 Aristotle은 71%, 최고 foundation model인 GPT 5.4는 56%를 기록했습니다.2 이는 AI가 강력한 보조자가 될 수는 있지만, 검증과 해석의 책임은 여전히 인간 연구자에게 있다는 점을 보여줍니다.
실용적인 판단 기준
AI-assisted proofs를 볼 때 중요한 질문은 “어떤 모델을 썼는가”만이 아닙니다. 실제 연구에 도움이 되려면 다음 요소가 함께 있어야 합니다.
상태 유지: 장기간 이어지는 가설과 수정 내역을 관리할 수 있는가
실패 기록: 틀린 접근과 반례를 남겨 다음 탐색에 반영하는가
작업 분해: 복잡한 문제를 병렬로 탐색 가능한 하위 문제로 나누는가
형식 검증: 자연어 설명을 넘어 기계적으로 확인 가능한 증명으로 연결되는가
인간의 최종 판단: 전문가가 의미, 엄밀성, 연구 가치까지 평가하는가
이 기준으로 보면 AI-assisted proofs는 수학자를 대체하는 기술이라기보다, 수학자의 탐색 범위를 넓히는 연구 인프라에 가깝습니다.
실제로 AI 도움을 받아 오랜 미해결 문제의 증명 과정을 설명한 사례도 나오고 있습니다. Nesterov accelerated gradient method의 점 수렴 문제를 해결한 논문은 ChatGPT의 도움을 크게 받았다고 밝힙니다.3
결국 관찰해야 할 변화는 “AI가 증명을 대신했는가”가 아닙니다. 상태 유지, 실패 기록, 형식 검증, 인간의 최종 판단이 하나의 연구 흐름 안에 들어오는지입니다. AI-assisted proofs의 미래는 단독 천재형 AI보다, 수학 연구를 더 체계적이고 협업적인 과정으로 바꾸는 도구에 가까워 보입니다.
1AI Co-Mathematician: Accelerating Mathematicians with Agentic AI
3Point Convergence of Nesterov's Accelerated Gradient Method: An AI-Assisted Proof
이 노트는 보도·비평·교육·연구 목적으로 작성되었습니다. 저작권 문의가 있으시면 에서 알려주세요.