현대 수학 연구에서 AI의 역할

### 수학 계산의 진화: 고대 도구부터 AI 지원까지
* 👨 영향력 있는 수학자이자 13세의 나이로 IMO 금메달리스트가 된 테렌스 타오 교수는 자신의 인생에서 **국제수학올림피아드(IMO)가 갖는 의미**와 참가자들에게 주는 즐거움에 대해 이야기합니다.
* 🤖 그의 강연은 수학에서 AI와 기계 지원이 미치는 혁신적 영향에 초점을 맞추며, **국제해사기구의 기하학 문제를 해결할 수 있는 DeepMind의 AlphaGeometry**와 같은 도구를 강조합니다.
* 타오는 **경쟁 수학은 빠른 문제 해결**이 필요한 반면, **연구 수학은 오랜 시간 탐구**해야 하기 때문에 문제 자체를 바꿔야 하는 경우가 많다고 설명합니다.
* 🕰 수학에서 기계의 사용은 수천 년 전으로 거슬러 올라가는데, **주판이 가장 초기의 사례** 중 하나이며 **컴퓨터의 개념은 지난 300~400년 동안 크게 발전**했습니다.
* 📊 그는 수학자들이 수열을 통해 서로 다른 수학 문제 사이의 연관성을 발견하는 데 도움을 주는 **온라인 정수 수열 백과사전(OEIS)**과 같은 데이터베이스의 역할에 대해 설명합니다.
* 🧑 타오는 1920년대부터 사용되어 온 과학적 계산의 중요성을 강조하며, **확장성 문제에 직면해 있지만 복잡한 논리 퍼즐을 해결하는 SAT 솔버의 출현**에 대해 언급합니다.
* 📜 그는 **네 가지 색 정리와 케플러 추측**과 같은 컴퓨터 지원 증명의 중요한 성과를 예로 들며 공식 증명 보조 도구와 최신 프로그래밍 언어를 통해 증명 검증 방법이 계속 발전하고 있음을 설명합니다.
* 🌐 마지막으로, 린과 같은 도구를 사용해 복잡한 수학적 증명을 공식화하는 최근의 발전을 강조하며 **공동의 노력이 어떻게 공식화 작업 흐름을 개선**하고 향후 연구를 위한 수학 라이브러리를 향상시킬 수 있는지 보여 줍니다.

### 수학의 미래: 대화형 증명, 머신 러닝 및 AI 혁신
* 🔍 수학의 진화는 사용자가 요소를 클릭하여 가설, 변수 및 공리에 대한 자세한 설명을 볼 수 있는 **대화형 증명 시스템**에 의해 형성되고 있으며, 미래의 교과서에서 이러한 매력적인 형식을 채택할 수 있는 길을 열어주고 있습니다.
* 🤝 최근 약 20명이 참여한 조합학 공동 프로젝트에서는 **단 3주 만에 복잡한 증명을 공식화**하여 수학 연구에서의 협업과 시각화를 향상시키는 대화형 시스템의 잠재력을 보여주었습니다.
* 📊 이 프로젝트는 종속성 그래프를 활용하여 큰 정리를 관리 가능한 부분으로 세분화함으로써 **컴퓨터 프로그래밍을 비롯한 다양한 분야의 기여자들이 전체 증명을 이해할 필요 없이 특정 부분만 작업**할 수 있도록 했습니다.
* 🔄 이 프로젝트에 사용되는 린 컴파일러는 **검증된 기여만 허용**되므로 이전에 함께 작업한 적이 없는 수학자들 간의 신뢰와 협업을 촉진할 수 있습니다.
* 📈 머신러닝은 수학, 특히 매듭 이론에서도 진전을 보이고 있는데, 방대한 데이터베이스에서 신경망을 학습시켜 **매듭 불변성을 예측**함으로써 수학적 구조 내에서 숨겨진 관계를 발견할 수 있는 AI의 잠재력을 입증하고 있습니다.
* 🧠 GPT-4와 같은 대규모 언어 모델은 수학 문제 해결을 위한 도구로 부상하고 있으며, **국제 수학 올림피아드와 같은 문제를 해결하는 데 어느 정도 성공**했지만 여전히 **기본적인 산술에 어려움**을 겪고 **정확한 결과를 얻기 위해서는 신중한 프롬프트**가 필요합니다.
* ⚙ 공식 증명 작성을 지원하는 AI 도구가 개발되고 있어 잠재적으로 프로세스의 속도를 높이고 수학자가 더 복잡한 작업에 집중할 수 있지만, **대규모 증명을 자동화하는 데는 상당한 어려움**이 남아 있습니다.
* 🌟 수학의 미래에는 **AI가 전례 없는 규모로 추측을 생성**하고 문제 클래스를 탐색하여 수학자들이 연구에 접근하고 복잡한 문제에 대해 협업하는 방식을 변화시킬 수 있습니다.

테렌스 타오 교수는 전통적인 방법과 최신 계산 도구를 연결하여 AI가 수학에 미치는 혁신적인 영향에 대해 강조합니다.

Terence Tao at IMO 2024: AI and Mathematics

AIMO Prize

테렌스 타오 교수의 수학에서의 AI와 기계 지원에 대한 강연

전 IMO 참여자이자 현재 UCLA 교수인 테렌스 타오 교수가 수학에서 AI와 기계 지원이 미치는 영향에 대해 이야기합니다.

그는 주판에서 현대 컴퓨터에 이르기까지 수학적 계산을 위해 기계를 사용해 온 오랜 역사를 강조합니다.

타오는 연구 수학에서 AI 도구의 혁신적 잠재력과 데이터베이스와 표를 통해 중요한 수학적 결과를 발견하는 데 있어 AI 도구의 역할을 강조합니다.

수학 문제 해결에서 컴퓨터의 역할

컴퓨터는 기하학 문제를 방정식 시스템으로 변환할 수 있지만, 그 복잡성은 크기에 따라 기하급수적으로 증가합니다.

SAT 솔버와 SMT 솔버는 논리 퍼즐을 풀고 일련의 가설에서 결론을 추론하는 데 사용되지만 확장성 측면에서 어려움을 겪기도 합니다.

최근 AI와 머신러닝의 발전은 공식 증명 도우미와 함께 수학에서 컴퓨터를 사용하는 새롭고 창의적인 방법을 제공하여 피타고라스 삼중 문제의 컴퓨터 증명과 같은 중요한 돌파구를 마련하고 있습니다.

그래프 환원성 증명과 같은 초기 수학적 증명은 지루한 수작업에 의존했으며, 90년대에 컴퓨터로 검증되었습니다.

17세기에 제안된 구체 포장에 대한 케플러의 추측도 최적성을 증명하는 데 어려움을 겪다가 1998년에 유연한 채점 방법과 컴퓨터 지원을 사용하여 성공적으로 증명되었습니다.

이 증명의 복잡성으로 인해 오랜 재검증 과정이 필요했고, 결국 컴퓨터 계산의 확실성에 대한 의문이 제기되었습니다.

컴퓨터를 이용한 증명에 대한 논란은 12년 만에 주요 정리를 공식화한 플라이스펙 프로젝트로 이어졌습니다.

피터 숄체의 응축 수학은 대수적 방법을 사용해 함수 분석 문제를 해결하는 것을 목표로 하며, 그 기초가 되는 중요한 소실 정리가 있습니다.

최신 증명 도우미인 Lean은 18개월 만에 이 정리를 성공적으로 공식화하여 수학 라이브러리에 추가하고 향후 공식화 프로젝트를 위한 청사진 워크플로우를 만들었습니다.

인터랙티브 교과서와 협업 증명의 미래

가설, 변수, 설명을 클릭할 수 있는 위치를 제공하는 대화형 교과서가 표준이 될 수 있습니다.

최근 20명이 참여한 조합론 프로젝트에서는 협업을 위한 의존성 그래프를 사용해 단 3주 만에 33페이지에 달하는 증명을 성공적으로 공식화했습니다.

Lean과 같은 공식 증명 도우미는 수학 수행 방식을 변화시켜 더 많은 협업과 더 빠른 증명의 조정을 가능하게 합니다.

머신러닝이 매듭 이론에 미치는 영향

머신러닝은 불변수와 다항식을 통해 매듭의 동등성을 탐구하는 매듭 이론을 연구하는 데 사용되고 있습니다.

매듭점 데이터베이스로 훈련된 신경망은 쌍곡선 기하학 불변수로부터 매듭점 시그니처를 성공적으로 예측했습니다.

이러한 블랙박스 접근 방식을 통해 주요 불변수를 식별하고 추측을 공식화하여 궁극적으로 매듭점 서명과 기하학적 불변수 사이의 관계에 대한 이론적 설명을 제공했습니다.

AI 모델은 기본적인 산술과 문제 해결에 어려움을 겪고 있으며, 종종 잘못된 답을 추측하기도 합니다.

신뢰할 수 있는 소프트웨어에 연결하고 증명 보조 언어를 사용하는 등 정확도를 높이기 위한 다양한 접근 방식이 모색되고 있습니다.

또한 AI는 문제 해결 기술의 뮤즈로서 유용하다는 것이 입증되고 있으며, 향후 좋은 추측을 생성하고 문제 공간을 탐색할 수 있는 잠재력을 가지고 공식 증명을 작성하는 데 도움을 주고 있습니다.

연사는 수학에서 전례 없는 발전을 가능하게 하는 AI 도구의 혁신적 잠재력에 대해 설명합니다.

또한 AI를 효과적으로 안내하는 전통적인 방법인 정리를 증명하는 것의 중요성을 강조합니다.

또한 동형 유형 이론에 대한 보보드스키의 영향, 수학 연구의 사회적 성격, 어린 나이에 대학에 진학한 연사 자신의 파격적인 경로에 대해서도 이야기합니다.