이 노트에 대하여
테런스 타오는 현대 수학의 대표적 거장으로, 보조증명과 계산 도구를 통해 수학 실천의 미래를 확장한다. 증명의 엄밀함과 계산 보조의 가능성을 함께 생각하게 한다.
히스토리
- @mitsein/claude-code/opus-5 — PFR Lean4 형식화 블로그, Equational Theories Project, AlphaProof 발표, ten advances 발표를 서지로 등록해 인물 좌표 절의 사실 주장에 인용을 달았다.
- @mitsein/claude-code/opus-5 — 히스토리·관련메타 5건·관련노트 8건을 세우고 인물 좌표 절을 넣었다. 2023-11 PFR 추측의 Lean4 형식화(Blueprint)와 2024-09-25 Equational Theories Project를 사실로 박고, 2026 ten-proofs 축과 이었다. 태그는 기존 것을 그대로 두었다.
- 렉스 프리드먼 팟캐스트 #472 기록
- 생성 — Machine Assisted Proof 콜로퀴엄 강연
관련메타
- † #수학
- † #증명 #설득 #귀류 #변증 #반증 #배리 — 증명보조기가 걸리는 자석. 이 노트가 원래 매달려 있던 자리다.
- † #인공지능 #수학 — AI가 수학을 돕는다는 주장이 놓이는 자리.
- † #형식언어 — 사람이 읽는 증명과 기계가 읽는 증명 사이.
- † #수리논리학 #기호논리학 #수학기초론
BIBLIOGRAPHY
“Formalizing the Proof of PFR in Lean4 Using Blueprint: A Short Tour.” 2023. November 18, 2023. https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/.
teams, AlphaProof, and AlphaGeometry. 2024. “AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems.” July 25, 2024. https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/.
“Ten Advances in Mathematics and Theoretical Computer Science.” 2026. August 1, 2026. https://openai.com/index/ten-advances-in-mathematics/.
Terence Tao: Hardest Problems in Mathematics, Physics & the Future of Ai. n.d. Accessed June 14, 2025. https://www.youtube.com/watch?v=HUkBz-cdB-k.
Terence Tao, “Machine Assisted Proof”. 2024. https://www.youtube.com/watch?v=AayZuuDDKP0.
관련노트
- @힣: 콕에서 베리코딩으로 — 백수의 형식증명 취미가 2년 뒤 선견지명이 된 자리 — 2026년 ten-proofs·베리코딩 방향축. 타오는 그 흐름을 2023년부터 현역 수학자 쪽에서 먼저 실행해 본 사람이다.
- @정주희 #수리논리 #집합론 #머신러닝 #수학 — 한국어 Coq 강의·용어집 축.
- @박성우 #콕 #논리학 — 한국어 Coq 자료의 다른 한 사람.
- §logickocli 한국어 자연어 추론 표준 논리 좌표계 — 자연어 논증을 형식 좌표계로 옮기는 도구 쪽.
- #변환: #수학수식 #형식언어 — 수학 명제를 형식언어로 옮기는 도구를 처음 물은 노트.
- @렉스프리드먼 Lex Fridman — 아래 팟캐스트 #472의 출처.
- @어니스트네이글 @ErnestNagel #괴델 #증명 — 형식체계 자체의 한계 쪽 축.
- @존스틸웰 수학자 #수학기초론 #논리 #증명 #역사 — 수학기초론을 역사 축으로 보는 자리.
왜 이 사람인가 — 기계보조증명을 직접 해 본 현역
1975년생, 2006년 필즈상, UCLA 교수. 이 노트에서 타오가 중요한 이유는 상이 아니라 자기 증명을 직접 형식화해 봤다 는 데 있다.
- 2023년 11월, PFR 추측. 팀 가워스·벤 그린·프레디 매너스와 함께 증명한 다항 프라이만–루자(PFR) 추측을 Lean 4로 옮기는 공동 프로젝트를 열었다. Yael Dillies·Bhavik Mehta와 함께였고, 파트릭 마소의 Blueprint 도구로 사람이 읽는 증명 개요와 Lean 코드를 링크했다. 시작 일주일도 되지 않아 논문의 상당 부분이 형식화됐고, 의존성 그래프가 어디까지 갔는지를 한눈에 보여 준다 (“Formalizing the Proof of PFR in Lean4 Using Blueprint: A Short Tour” 2023).
덧붙여, 같은 해 7월 25일 딥마인드가 AlphaProof로 IMO 은메달 수준에 도달했다고 발표했다 (teams and AlphaGeometry 2024) — 아래 강연이 형식 증명 보조기를 다루는 맥락이 그 직후다.
- 2024년 9월 25일, Equational Theories Project. 마그마의 등식 이론 4,694개 사이의 함의 22,028,942개를 Lean으로 판정하는 크라우드소싱 프로젝트를 시작했다. “Lean으로 검증된 것”과 “사람 또는 기계가 추측한 것”을 대시보드에서 분리해 표시한다 (“Equational Theories Project” 2024).
즉 타오는 형식화를 증명의 장식이 아니라 협업 규모를 바꾸는 장치 로 썼다. 한 사람이 전부 읽어야 했던 증명을 조각으로 쪼개고, 조각의 진위는 커널이 판정하게 하고, 사람은 어디까지 왔는지를 그래프로 본다.
아래 2024년 콜로퀴엄 강연이 그 관점을 정리한다. 인간 계산기에서 SAT 솔버, 머신러닝, LLM, 형식 증명 보조기까지를 한 계보로 놓되 인간의 직관이 남는 자리를 지운 적이 없다. 2026년 8월 OpenAI가 Lean 증명서와 독립 커널 재검사를 붙여 열 개의 결과를 공개했을 때 (“Ten Advances in Mathematics and Theoretical Computer Science” 2026), 그것을 읽을 준비된 독법이 이미 여기 있었다.
2024 “Terence Tao, “Machine Assisted Proof” 기계 형식 증명 보조기
(Terence Tao, “Machine Assisted Proof” 2024)
타오는 먼저 수학적 계산의 역사적 맥락을 제공하며, 인간 “컴퓨터”에서 전자 기계로의 진화를 강조합니다. 그는 실험 수학에서 표와 대규모 데이터베이스의 중요성을 언급하며, 가우스와 B. 스위너튼-다이어의 작업과 같은 역사적 사례를 소개합니다.
이어서 그는 수치 및 과학 계산에서 컴퓨터의 사용과 반올림 오류의 영향, 그리고 구간 산술을 통한 계산 신뢰성 향상 가능성을 논의합니다. 타오는 SAT 솔버와 같은 고급 도구와 그 응용, 특히 부울 피타고라스 삼중수 문제 해결에 대해 소개합니다.
타오는 수학에서 새로운 세 가지 기술적 양상, 즉 기계 학습 알고리즘, 대규모 언어 모델(LLM), 그리고 형식적 증명 보조기에 대해 설명합니다. 이러한 기술이 매듭 이론과 편미분 방정식 등의 수학 연구를 지원할 수 있는 잠재력을 논의합니다.
그는 컴퓨터 보조 증명의 역사적 사용을 언급하며, 4색 정리와 케플러 추측과 같은 중요한 결과와 정확성 보장을 위한 형식적 검증의 중요성을 강조합니다.
강연은 미래 수학에 대한 논의로 마무리되며, 형식적 증명 시스템을 통한 협업 가능성과 AI 도구의 통합을 통한 수학적 추론 및 탐구 향상 잠재력을 강조합니다. 타오는 기술의 지속적인 발전이 수학 실천을 변화시킬 것이라는 긍정적인 견해를 표현하면서도, 이 과정에서 인간의 직관이 여전히 필요하다는 점을 인정합니다.
- 수학 콜로퀴엄 강연은 1895년 AMS 첫 회의부터 이어져 온 전통으로, 저명한 수학자들을 소개하는 자리입니다.
- 저명한 수학자 테리 타오는 기계와 컴퓨터 보조 수학의 발전 과정을 논의하며, 그 역사적 의의와 최근 발전 사항을 강조했습니다.
- 수학에서 컴퓨터 활용은 사람이 직접 조작하는 장치에서 복잡한 전자 시스템으로 발전했으며, 이를 통해 방대한 데이터 생성과 분석이 가능해졌습니다.
- 실험 수학은 소수 테이블과 정수 수열 온라인 백과사전 등 대규모 데이터베이스에 의존합니다.
- 과학 컴퓨팅은 복잡한 시스템 모델링에 핵심적인 역할을 하며, 구간 산술 등의 방법으로 수치 정확도를 향상시킵니다.
- 최근 충족가능성(SAT) 솔버 발전은 수학 문제 해결에 혁신을 가져왔으며, 부울 피타고라스 삼중수 문제 해결이 그 대표적인 예입니다.
- 기계 학습과 대규모 언어 모델(LLM)은 수학 연구에서 추측 생성과 보조 도구로 활용되고 있지만, 그 효과는 다양합니다.
- 형식 증명 보조기가 부상하면서 수학적 증명의 엄밀한 검증과 수학자 간 대규모 협업이 가능해졌습니다.
- LLM과 증명 보조기 등 다양한 컴퓨팅 도구의 통합은 수학 연구의 효율성을 높일 수 있는 혁신적인 접근법을 제시할 것입니다.
- 미래 수학은 인간의 직관과 자동화된 프로세스의 결합을 통해 발전할 것이며, AI가 아이디어 생성을 보조할 수 있지만 유의미한 통찰을 구별하는 과제가 여전히 남아 있습니다.
Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI | Lex Fridman Podcast #472
(Terence Tao: Hardest Problems in Mathematics, Physics & the Future of Ai n.d.) Terence Tao
Comments