[뉴스스페이스=이종화 기자] 스스로를 "AI 수학자"를 구축하고 있다고 칭하는 AI 스타트업 액시엄(Axiom)은 2월 3일(현지시간) 자사의 시스템 액시엄 Prover가 이전에 풀리지 않은 수학 문제 4개를 해결했다고 발표하며, 인공지능의 형식적 추론 능력에서 새로운 이정표를 세웠다.

wired, thegamingboardroom, forbes, arxiv.org가 보도한 이 발표에는 수년간 인간 수학자들이 풀지 못했던 대수기하학과 정수론의 오랜 추측들에 대한 해법이 포함되어 있다. 해결된 문제 중에는 수학자 Dawei Chen과 Quentin Gendron의 논문에 나온 리만 곡면 위 k-미분의 스핀 패리티에 관한 추측이 있는데, 이 결과는 수학자들이 증명할 수 없었던 정수론적 가설에 조건부로 의존하고 있었다.

액시엄은 2025년 3월 스탠포드 중퇴생 카리나 홍(Carina Hong)이 설립한 이래 9개월 만에 6,400만 달러(약 880억원) 시드 펀딩을 유치하며 메타 FAIR 연구원들을 영입했다. 버지니아대 교수 출신 켄 오노(Ken Ono) 정수론 전문가를 창립 수학자로 초빙한 점도 주목받는다.
​

45년 만 증명…Erdős 문제 #481, 단 5시간 만에 656줄 코드 생성

액시엄Prover는 에르되시 문제(Erdős Problems) #481(약 45년 미해결)을 5시간 만에, #124(약 30년 미해결)를 24시간 만에 Lean 형식 증명으로 풀어냈다. #481 증명은 656줄로 '간결하고 우아하다'고 평가됐으며, 이는 GPT-5의 기존 문헌 검색과 달리 순수 AI 독창성을 입증한다.
​

또한 130년 된 Lyapunov 함수 안정성 문제와 30년 그래프 이론 추측 반증도 포함된 4개 해결 사례는 AI의 형식 추론 능력을 보여준다. 에르되시는 생전 1,100개 문제를 제기했는데, 현재까지 266개만 해결된 상태다.

arXiv 논문 공개…인간-AI 협력 워크플로우 강조

2026년 2월 3일 arXiv에 게재된 논문(Parity of k-differentials in genus zero and one)에서 액시엄은 추측 명제만 입력으로 야코비 기호 재구성을 자율 발견했다고 밝혔다. Lean 4.26.0으로 검증된 solution.lean 파일은 GitHub(https://github.com/액시엄Math/parity-differential)에 공개됐다.

논문 저자 다웨이 천(Dawei Chen)은 "액시엄Prover가 인간이 간과한 핵심 관찰을 찾아냈다"고 평가했다. 이는 Putnam 2025 12문제 전부 해결(Lean 증명 공개) 사례와 맞물려 AI 수학의 실전 가능성을 높인다.

오픈AI 비판 딛고…인간 검증 필수, 연구 도우미 역할

오픈AI가 2025년 말 기존 문헌 검색으로 비판받은 데 비해 액시엄은 Lean 형식 검증으로 차별화됐다. 그러나 홍 대표는 "AI는 인간 연구자를 대체가 아닌 협력 도구"라며 연구 워크플로우 원리 증명을 강조했다.
​

전문가들은 AI가 재현성·피어 리뷰를 거쳐야 한다고 지적한다. 액시엄의 성공은 수학-AI-Science 이론 층 결합으로 금융·하드웨어 검증 등 응용 확대를 예고하고 있다.