Harmonic AI, 30년 된 수학 문제 4개 자율 해결

작성자:

Harmonic AI, 30년 된 수학 문제 4개 해결: AI 수학 시대 열렸다

  • Harmonic의 Aristotle AI가 에르되시(Erdős) 문제 4개를 자율적으로 해결
  • 문제 #728은 AI가 완전 자율로 해결한 최초의 에르되시 문제
  • 필즈상 수상자 테렌스 타오가 직접 증명 검증

무슨 일이 일어났나?

수학 AI 스타트업 Harmonic이 개발한 Aristotle AI가 2026년 1월 한 달 동안 미해결 에르되시 문제 4개를 연달아 해결했다.[arXiv] 에르되시 문제는 전설적인 헝가리 수학자 폴 에르되시가 남긴 1,133개의 난제 컬렉션이다. 그중 680개가 아직 미해결 상태였다.

가장 주목할 만한 성과는 문제 #728이다. 1월 4일 케빈 바레토가 Aristotle을 이용해 증명을 발표했고, 1월 6일에는 Lean 4 프로그래밍 언어로 형식 검증까지 완료했다.[Hacker News] 이는 AI가 인간 도움 없이 완전 자율로 에르되시 문제를 해결한 최초 사례다.

뒤이어 문제 #729, #397, #124가 차례로 해결됐다. 문제 #124는 1990년대부터 30년간 미해결이었는데, Aristotle이 단 6시간 만에 풀어버렸다.[36Kr]

왜 중요한가?

AI가 수학 문제를 푸는 건 새롭지 않다. DeepMind의 AlphaEvolve도 50개 이상의 수학 퍼즐에서 인간보다 나은 결과를 냈다. 하지만 Aristotle의 차별점은 형식 검증에 있다.

기존 LLM은 그럴듯한 답을 내놓지만 환각을 피할 수 없다. Aristotle은 Lean 4 증명 보조기를 통해 수학적으로 완벽한 증명을 생성한다. 필즈상 수상자 테렌스 타오가 문제 #397의 증명을 하루 만에 검토하고 승인한 것도 이 검증 가능성 덕분이다.

Harmonic은 2025년 11월 시리즈 C에서 14.5억 달러 가치로 1.2억 달러를 투자받았다. 2026년 1월에는 Nvidia의 NVentures까지 투자자로 합류했다.[SiliconANGLE]

앞으로 어떻게 될까?

Harmonic의 공동창업자 블라드 테네브(Robinhood CEO)와 튜더 아킴은 수학적 초지능을 목표로 한다. 수학 검증 기술은 코딩, 칩 설계, 안전-핵심 소프트웨어 검증으로 확장될 전망이다.

다만 테렌스 타오는 현재 해결된 문제들은 가장 쉬운 열매라고 경고했다. 표준 기법으로 풀 수 있는 문제들이며, 진정한 수학적 돌파구와는 거리가 있다. AI는 문제 프레이밍과 전문가 검증에서 여전히 인간에게 의존한다.

자주 묻는 질문 (FAQ)

Q: Aristotle AI는 어떻게 수학 문제를 푸나?

A: Aristotle은 강화학습, 몬테카를로 트리 탐색, Lean 4 형식 언어를 결합한다. 자연어로 된 수학 문제를 형식적으로 검증 가능한 증명으로 변환한다. GPT-5.2가 초기 증명을 생성하면 Aristotle이 Lean으로 형식 검증하는 방식으로 협업하기도 한다.

Q: Harmonic AI는 어떤 회사인가?

A: 2023년 설립된 팔로알토 기반 스타트업이다. Robinhood CEO 블라드 테네브가 공동창업자 겸 이사회 의장이고, 튜더 아킴이 CEO다. 시리즈 C에서 14.5억 달러 기업가치를 인정받았으며, Nvidia, Sequoia, Index Ventures가 투자했다.

Q: 에르되시 문제란 무엇인가?

A: 헝가리 수학자 폴 에르되시가 평생 제시한 수학 난제 컬렉션이다. 현재 1,133개가 카탈로그화되어 있고, 279개가 해결됐으며 680개가 미해결 상태다. 정수론, 조합론, 그래프 이론 등 다양한 분야를 포괄한다.

이 글이 유용했다면 AI Digester를 구독해주세요.

참고 자료

댓글 남기기