AI, 수학 난제 해결의 새로운 지평을 열다

커뮤니티에서는 ChatGPT, Sol, Fable과 같은 LLM이 Erdős의 Unit Distance 추측 및 Jacobian Conjecture와 같은 난제에 대한 반례를 신속하게 발견하는 능력을 높이 평가하고 있습니다. 특히, 100페이지 분량의 복잡한 이론을 자동 형식화(Autoformalization)하는 과정에서 AI가 인간보다 더 빠르고 정확하게 오류를 찾아내는 사례가 주목받고 있습니다. 이는 수학 연구의 패러다임 전환(Paradigm Shift)을 예고하는 중요한 지표로 해석됩니다.

AI가 생성한 수학적 결과의 신뢰성을 확보하기 위해 Lean과 같은 형식 검증 도구(Formal Verification Tools)의 역할이 강조되고 있습니다. AI가 생성한 수백만 줄의 Lean 코드를 검증하는 과정은 필수적이며, 이는 AI가 생성한 코드가 임의 명령을 실행할 수 있다는 점에서 보안(Security) 측면에서도 중요합니다. mathlib과 같은 방대한 라이브러리의 존재는 이러한 형식 검증을 더욱 용이하게 합니다.

AI가 수학적 발견의 속도를 높이면서, 인간 수학자의 역할은 새로운 추측의 공식화, AI 결과의 해석, 그리고 창의적인 탐구로 이동할 것이라는 전망이 나옵니다. 일부에서는 AI가 발견한 반례가 '저공 비행 과일(low-hanging fruit)'에 해당하며, 인간의 깊은 통찰력과는 다르다고 주장하지만, AI 도구 활용 능력이 미래 수학자의 중요한 역량이 될 것이라는 데는 이견이 적습니다.

AI가 생성한 수학적 결과물은 때때로 '끔찍한(horrible)' 코드를 포함하거나, 인간의 직관과는 다른 방식으로 접근할 수 있습니다. 그러나 데이터 격리 아키텍처(Data Isolation Architecture)를 통해 안전하게 실행된 AI 생성 코드는 수백만 줄의 Lean 코드를 단기간에 완성하며 수십 년간 미해결된 문제를 해결하는 데 기여했습니다. 이는 AI가 단순한 도구를 넘어 수학적 발견의 동반자가 될 수 있음을 시사합니다.

AI 도구를 활용한 수학 연구는 연구자 간의 협업을 촉진하고 있습니다. 예를 들어, Akhil Mathew는 AI 도구를 사용하여 Grothendieck의 질문에 대한 반례를 발견하고 이를 mathlib에 기여했으며, Levent Alpöge는 Fable을 통해 Jacobian Conjecture의 반례를 찾아냈습니다. 이러한 사례는 AI가 새로운 수학적 통찰(Mathematical Insight)을 제공하고, 인간 연구자들이 이를 바탕으로 더 깊은 이해를 추구하도록 이끌고 있습니다.