AI로 수학 미해결 문제 거의 자동 해결 성공했다

20세기에 가장 많은 논문을 쓴 수학자로 알려진 폴 에르되시는 생애 동안 많은 미해결 문제를 제시했으며 이들은 에르되시 문제(Erdős Problem)로 알려져 있다. 이런 에르되시 문제 중 한 문제를 GPT-5.2 Pro가 해결했고 저명한 수학자인 테런스 타오는 자신이 아는 한 기존 문헌에서는 재현되지 않는 거의 자율적인 해결이며 AI 능력이 실제로 향상됐다는 걸 보여주는 것이라고 평가했다.

이번에 화제가 된 에르되시 문제 728번은 1975년 에르되시 등이 제기한 팩토리얼 정제성에 관한 정수론 문제로 충분히 작은 상수 C와 ε이 존재할 때 a!b!가 n!(a+b-n)!을 나누어떨어뜨린다 그리고 a+b가 n+C*log n보다 크다를 만족하는 정수 (a,b,c)가 무한히 존재하는가라는 것. 다만 타오에 따르면 원래 문제는 표현이 모호했다. 예를 들어 상수 C가 작은 상수로 의도된 것인지 큰 상수로 의도된 것인지가 분명하지 않았다고 한다.

이 문제 해결에는 GPT-5.2 Pro와 Aristotle이라는 AI 도구가 주도적인 역할을 했다. 한 레딧 사용자(ThunderBeanage)는 지금까지 다양한 LLM을 사용하여 수학 증명을 시도해왔다. 하지만 그에 따르면 기존 LLM에 인터넷 검색을 허용하면 문제가 미해결임을 알아차리고 해결할 수 없다고 판단해 해법 탐색을 중단해버리는 경우가 있었다고 한다. 따라서 프롬프트에서 인터넷 검색을 하지 않도록 지시하거나 인터넷을 차단해 그런 행동을 피했다고 한다. 또 인터넷을 차단해도 이번에는 환각이나 치명적인 비약이 빈발해 올바른 증명이 되지 않는 게 큰 장애물이었다고 한다.

하지만 2025년 12월 등장한 GPT-5.2 Pro는 증명을 만드는 도중 메울 수 없는 보조정리가 있을 경우 무리하게 조작하지 않고 여기가 미해결이라고 솔직히 말하는 경향이 있었으며 전체 골격은 상당한 비율로 정확했다고 한다. 따라서 최종적으로 인터넷을 사용하는 GPT-5.2로 문제 의도와 방침을 정리하고 LaTeX로 기술한 짧은 프롬프트를 만든다→별도 인스턴스 GPT-5.2에 인터넷을 금지한 상태에서 해당 프롬프트를 제공해 증명을 작성시킨다→별도 인스턴스에 검산과 수정을 시킨다는 방법을 고안했다.

1월 4일에는 GPT-5.2 Pro가 제약이 있는 증명을 출력했다. 다만 이때는 문제의 모호함이 원인으로 올바르게 해결했다고 간주되지 않았기 때문에 a,b≤(1-ε)n이라는 더 엄격한 조건을 부과한 해석으로 해결을 도모하게 됐다.

이를 다른 사용자(AcerFur)가 Aristotle에 전달해 Lean으로 형식화했다. 하지만 이후 커뮤니티 내에서 논쟁이 발생했고 상수 C를 어떻게 해석할 것인가에 대해 다시 엄격한 제약을 부과할 필요가 생겼다고 한다.

이에 따라 GPT-5.2 Pro에 추가 제약을 만족하는 형태로 논증을 업그레이드할 수 있는지를 다시 물었더니 GPT-5.2 Pro는 가능하다고 답했다. 출력된 새로운 증명이 Aristotle에 의해 형식화됐다. 그때 증명에는 작은 오류가 섞여 있었지만 Aristotle이 자동으로 간극을 수정해 Lean으로 검증된 형태로 완성했다고 한다.

에르되시 문제에 취조하고 있는 타오는 이번 증명에 대해 AI가 에르되시 문제를 거의 자율적으로 해결했다고 평가했다. 그 중에서도 기존 문헌에는 찾아볼 수 없는 결론이 AI에 의해 도출된 것, 나아가 추가 지시나 대화를 거듭해 빈틈을 메우거나 참조를 정리해 논문을 단시간에 여러 번 다시 쓰고 개선할 수 있었던 것을 흥미로운 진보로 평가했다.

타오는 중요한 부분은 인간이 주체적으로 쓰는 형태가 바람직하다고 하면서도 기존에는 읽기 쉬운 원고 한 편을 완성하는 것만으로도 큰 노력이 들었고 그 후의 개고도 국소적인 수정에 그치기 쉬웠던 것에 비해 AI를 사용하면 큰 구성 변경을 포함한 재작성을 빠르게 반복할 수 있다는 점을 높이 평가했다. 관련 내용은 이곳에서 확인할 수 있다.