[배경지식 한 입] AI 수학에서 새롭게 떠오른 증명의 검증과 이해

청랑 배경지식 · 서양 근현대사에서 읽는 오늘의 AI와 수학적 증명

AI가 증명을 쏟아내는 시대에는 ‘풀었는가’보다 ‘누가 검증하고 무엇을 이해했는가’가 수학의 새로운 병목이 된다

1900년 힐베르트의 23개 문제에서 1976년 4색정리의 컴퓨터 증명, 1998~2014년 케플러 추측의 형식검증까지 이어지는 ‘증명이란 무엇인가’의 역사

인공지능이 고등수학의 공개문제를 한두 개가 아니라 수백 개 규모로 공략하는 상황이 현실이 되고 있다. 오픈AI는 2026년 10월 내부 프런티어 모델이 만든 광범위한 수학 연구결과를 공개했다. 공개 저장소에는 대수학·수론·수리논리·기하학·이론컴퓨터과학 등 여러 분야의 결과가 수백 개의 묶음으로 정리돼 있다.

그러나 이를 곧바로 “AI가 수학 난제 300개를 모두 해결했다”고 이해하는 것은 정확하지 않다. 공개된 자료에는 장기간 미해결이던 문제를 해결했다고 주장하는 결과도 있고, 기존 정리를 강화하거나 특정 조건에서 진전을 보인 결과도 있으며, 서로 관련된 여러 논문이 하나의 결과군으로 묶인 경우도 있다. 무엇보다 상당수는 이제 막 공개된 원고로, 수학계의 독립적인 검토와 평가가 진행 중이다.

대표적인 예가 ‘준리만 가설’이다. 오픈AI가 공개한 결과는 리만 제타함수를 포함한 특정 L-함수들이 복소평면의 실수부가 7/8보다 큰 영역에서는 영점을 갖지 않는다는 내용을 제시한다. 이것은 중요한 진전으로 제시되고 있지만, 밀레니엄 문제인 리만 가설 자체를 증명한 것은 아니다. 리만 가설은 모든 비자명한 영점의 실수부가 정확히 1/2이라는 훨씬 강한 명제다.

나비에-스토크스 문제도 단계 구분이 필요하다. 오픈AI는 9월 내부 AI 시스템이 유체의 운동을 나타내는 나비에-스토크스 방정식에서 유한시간 안에 특이점이 발생할 수 있음을 보이는 해법을 찾았다고 발표하고 논문과 Lean 형식검증 자료를 공개했다. 클레이수학연구소도 이 결과에 대해 문제가 ‘해결된 것으로 보인다’는 취지의 공식 논평을 냈다.

그렇지만 100만달러의 밀레니엄 상이 즉시 확정되는 것은 아니다. 클레이수학연구소의 공식 규칙은 제안된 해법이 적절한 학술매체에 출판되고, 출판 뒤 최소 2년이 지나며, 세계 수학계에서 일반적인 승인을 받아야 심사대상이 될 수 있도록 규정한다. 즉 AI가 답을 만들어 내는 시점과 그 답이 수학적 지식으로 정착하는 시점은 다르다.

수학자들의 우려도 바로 이 간격에서 나온다. AI가 인간 연구자가 읽고 이해하는 속도보다 훨씬 빠르게 새로운 논문을 생산하기 시작하면, 연구의 가장 부족한 자원이 ‘새로운 증명 찾기’에서 ‘증명 읽기·검증하기·기존 연구와 연결하기’로 이동할 수 있다. 누가 먼저 같은 아이디어를 연구했는지 확인하는 인용과 연구윤리 문제도 훨씬 복잡해진다.

오픈AI는 이런 논쟁 뒤 프린스턴 고등연구소를 거점으로 활동하는 독립적인 수학·AI 자문그룹과 협의해 공개방식을 조정하고 있다. 자문그룹은 이번 공개가 결과의 가치를 보증하는 행위가 아니며, 자료를 공개하는 것은 인간이 이해하고 수학적 지식으로 편입하는 과정의 완료가 아니라 시작이라고 강조했다.

이 논쟁은 사실 완전히 새로운 것이 아니다. 지난 120여 년 동안 수학은 ‘무엇이 중요한 문제인가’, ‘컴퓨터가 확인한 결과를 증명이라 부를 수 있는가’, ‘사람이 읽을 수 없는 증명을 기계가 논리적으로 검증하면 충분한가’를 반복해서 고민해 왔다. 오늘의 AI 논란을 이해하는 데 결정적인 역사적 사례가 바로 힐베르트의 문제 목록, 4색정리, 그리고 케플러 추측의 형식검증이다.

AI의 수학 난제 도전을 이해하는 세 가지 역사적 배경지식

오늘의 쟁점	관련 역사·개념	깊이 이해할 관계
AI가 수백 개 공개문제를 한꺼번에 공략한다	서양 근현대 · 1900년 힐베르트 23개 문제 · 2000년 밀레니엄 7대 난제 · 연구의제 설정	수학에서 유명 난제는 왜 단순한 ‘정답 맞히기 대회’가 아니라 여러 세대가 새로운 개념과 방법을 개발하도록 만드는 연구의제가 되었는가
AI의 증명이 너무 길거나 복잡해 인간이 직접 확인하기 어렵다	서양 근현대 · 1976년 Appel-Haken의 4색정리 · 최초의 대규모 컴퓨터 보조 증명	논리적으로 옳은 결과와 인간이 전체 과정을 직접 이해하고 검사할 수 있는 증명은 반드시 같은 것인가
Lean 같은 증명보조기가 AI 논증의 정확성을 확인한다	서양 근현대 · 1998년 케플러 추측 증명 · Flyspeck 프로젝트 · HOL Light·Isabelle 형식검증	컴퓨터가 모든 논리단계를 확인하면 무엇이 해결되고, 독창성·설명·의미·연구윤리처럼 무엇은 여전히 인간의 판단으로 남는가

1. 힐베르트가 1900년에 난제 목록을 만든 이유는 정답 23개가 필요해서가 아니라 앞으로 수학이 어디로 갈지를 묻기 위해서였다

오늘날 AI 회사가 얼마나 많은 미해결 문제를 풀었는지가 성능의 상징처럼 받아들여지는 데에는 수학 특유의 전통이 있다. 수학에서는 오랫동안 중요한 공개문제를 목록으로 만들고, 그 문제를 해결하거나 큰 진전을 이루는 일을 학문의 최전선으로 여겨 왔다.

그 전통의 가장 유명한 출발점 가운데 하나가 독일 수학자 다비트 힐베르트가 1900년 파리 국제수학자대회에서 제시한 문제들이다. 힐베르트에게 난제는 단순히 아무도 풀지 못한 퍼즐이 아니었다. 앞으로 어떤 새로운 개념과 방법이 수학을 발전시킬지를 보여 주는 표지판이었다.

힐베르트와 클레이수학연구소는 왜 굳이 ‘가장 어려운 문제 목록’을 만들어 수학계에 던졌을까?

JWSBOOKS EDITOR'S PICK 하루 15분, 시사 논술 필사 현대 사회의 주요 시사 이슈를 하루 15분, 30일 동안 필사하며 체득하도록 구성된 실전 글쓰기·문해력 훈련서입니다.

청랑북스 살펴보기

좋은 난제는 정답 개수를 세기 위한 목록이 아니라 새로운 수학을 만들어 내는 연구의제다

1900년 힐베르트의 문제 목록과 2000년 클레이수학연구소의 밀레니엄 문제는 ‘누가 몇 문제를 풀었는가’를 겨루는 퀴즈 목록이 아니었습니다. 해결을 시도하는 과정에서 새로운 개념·언어·증명기법을 만들고 여러 세대의 연구방향을 조직하는 연구의제에 가까웠습니다.

푸앵카레 추측도 페렐만이 2002~2003년 해법을 공개한 순간 바로 공식 종료된 것이 아니라 여러 연구자가 세부논증을 검토하고 재구성한 뒤 2010년에야 밀레니엄상 해결로 공식 인정됐습니다. 풀이의 등장과 학문공동체의 승인 사이에는 검증의 시간이 존재합니다.

AI가 단기간에 수백 개의 후보 결과를 만들 수 있다면 병목은 ‘아이디어 생산’에서 ‘어떤 결과가 새롭고 중요한지 선별하고 이해하는 일’로 이동할 수 있습니다. 그래서 AI 시대에도 난제의 가치는 해결 개수보다 어떤 새로운 수학을 낳았고 공동체가 어떻게 받아들였는가에 달려 있습니다.

청랑학습코칭 아카이브 힐베르트 문제와 수학의 연구의제를 더 깊이 알아보세요 1900년 힐베르트의 23개 문제와 2000년 밀레니엄 7대 난제를 통해 유명 난제가 왜 정답 맞히기보다 새로운 이론과 방법을 끌어내는 연구의제로 작동하고, 해결 뒤에도 공동체 검증이 필요한지 아카이브에서 이어서 살펴보세요. 배경지식 더 알아보기 →

2. 1976년 4색정리는 컴퓨터가 옳은 답을 증명했는데도 ‘사람이 직접 확인하지 못하는 것을 증명이라 부를 수 있는가’라는 논쟁을 일으켰다

AI가 만든 증명을 놓고 “논리적으로 맞다고 기계가 확인했다면 충분한가”라는 질문은 처음 등장한 것이 아니다. 거의 정확히 50년 전 수학계는 비슷한 충격을 경험했다.

문제는 초등학생도 이해할 만큼 간단했다. 평면의 지도를 인접한 두 지역이 같은 색이 되지 않도록 칠하려면 네 가지 색이면 항상 충분한가라는 ‘4색 문제’였다. 질문은 쉬웠지만 증명은 120년 넘게 발견되지 않았다.

1976년 컴퓨터가 1,936개 경우를 확인했을 때 왜 ‘증명은 맞아도 우리가 이해했다고 할 수 있나’라는 논쟁이 생겼을까?

JWSBOOKS EDITOR'S PICK 하루 15분, 시사 논술 필사 현대 사회의 주요 시사 이슈를 하루 15분, 30일 동안 필사하며 체득하도록 구성된 실전 글쓰기·문해력 훈련서입니다.

청랑북스 살펴보기

4색정리는 ‘참임을 확인하는 증명’과 ‘왜 참인지 이해시키는 증명’이 다를 수 있음을 드러냈다

1976년 아펠과 하켄은 4색 문제를 유한한 경우들로 환원한 뒤 1,936개의 구성을 컴퓨터로 검사해 정리를 증명했습니다. 결과는 수학적으로 받아들여졌지만, 사람이 계산 전체를 직접 따라가기 어렵다는 점 때문에 컴퓨터가 확인한 것을 어디까지 증명으로 볼 것인가라는 논쟁이 시작됐습니다.

이 논쟁은 정확성과 이해가 서로 다른 가치일 수 있음을 보여 줬습니다. 컴퓨터는 방대한 경우를 빠짐없이 검사해 오류 가능성을 줄일 수 있지만, 인간이 원하는 좋은 증명은 종종 왜 그 정리가 참인지 구조적 이유와 통찰까지 설명하기를 요구합니다.

오늘날 AI가 길고 복잡한 증명을 만들 때도 같은 문제가 되풀이됩니다. 형식적으로 옳다고 확인된 결과는 강한 신뢰를 줄 수 있지만, 그 안에서 어떤 아이디어가 핵심인지, 더 짧은 원리가 있는지, 다른 문제에 어떻게 일반화할지는 여전히 인간이 해석해야 합니다.

청랑학습코칭 아카이브 4색정리와 컴퓨터 보조 증명의 의미를 더 깊이 알아보세요 1976년 아펠-하켄의 4색정리와 이후 Coq 형식증명을 통해 컴퓨터가 증명의 정확성을 높일 수 있으면서도 인간이 ‘왜 참인가’를 이해하고 설명하는 문제는 별도로 남을 수 있는 이유를 아카이브에서 살펴보세요. 배경지식 더 알아보기 →

3. 케플러 추측은 컴퓨터가 포함된 증명을 발표한 뒤에도 16년 동안 형식검증을 거치며 ‘기계가 기계를 검증하는 수학’의 길을 열었다

컴퓨터 계산이 포함된 증명에서 가장 현실적인 걱정은 “프로그램을 믿어도 되는가”다. 사람이 모든 계산을 다시 할 수 없다면 프로그램 자체에 버그가 없는지를 어떻게 보장할 것인가라는 문제가 남는다.

이 문제를 해결하는 한 방법이 형식검증(formal verification)이다. 수학적 명제와 증명을 컴퓨터가 읽을 수 있는 엄밀한 언어로 바꾸고, 매우 작은 검증 프로그램이 모든 논리단계가 공리와 앞 단계에서 정확히 따라오는지를 확인하게 한다. 오늘날 Lean·Coq·HOL Light·Isabelle 같은 증명보조기가 이 역할을 한다.

1998년 케플러 추측 증명은 왜 논문 발표 뒤에도 Flyspeck이라는 16년짜리 형식검증 프로젝트를 다시 거쳐야 했을까?

JWSBOOKS EDITOR'S PICK 하루 15분, 시사 논술 필사 현대 사회의 주요 시사 이슈를 하루 15분, 30일 동안 필사하며 체득하도록 구성된 실전 글쓰기·문해력 훈련서입니다.

청랑북스 살펴보기

형식검증은 AI 증명의 논리적 오류를 줄이지만 독창성·중요성·의미까지 대신 판단하지는 않는다

케플러 추측은 1998년 헤일스와 퍼거슨이 컴퓨터 계산을 포함한 증명을 발표한 뒤에도 전통적인 심사만으로 모든 계산을 완전히 재확인하기 어려웠습니다. 그래서 2003년 시작된 Flyspeck 프로젝트는 증명 전체를 형식언어로 옮겨 기계가 모든 논리단계를 검사하도록 했습니다.

2014년 완성된 형식검증은 HOL Light와 Isabelle 같은 증명보조기가 복잡한 논증의 각 단계가 공리와 이전 단계에서 실제로 따라오는지를 확인할 수 있음을 보여 줬습니다. 오늘날 Lean이 AI가 만든 긴 증명을 검증하는 데 주목받는 이유도 그럴듯함이 아니라 형식적 추론규칙을 검사하기 때문입니다.

하지만 형식검증이 통과했다고 학술적 평가가 모두 끝나는 것은 아닙니다. 원래 문제를 정확히 형식화했는지, 결과가 기존 연구보다 새로운지, 핵심 아이디어의 우선권이 누구에게 있는지, 왜 중요한지는 별도의 판단입니다. 검증 가능한 증명과 이해 가능한 수학은 함께 필요합니다.

청랑학습코칭 아카이브 Flyspeck과 Lean 형식검증을 더 깊이 알아보세요 케플러 추측의 1998년 컴퓨터 보조 증명부터 2014년 Flyspeck 완성까지의 과정을 통해 형식검증이 무엇을 보장하고, 독창성·설명·선행연구·학술적 중요성 같은 어떤 판단은 여전히 인간에게 남는지 아카이브에서 이어서 살펴보세요. 배경지식 더 알아보기 →

AI가 수학자를 없애는가보다 더 중요한 변화는 ‘증명을 만드는 사람’과 ‘증명을 이해하고 지식으로 편입하는 사람’의 역할이 분리될 수 있다는 점이다

2026년의 AI 수학 논쟁에서 가장 먼저 구분해야 할 것은 ‘후보 해법의 등장’, ‘형식적인 정확성 확인’, ‘전문가의 이해’, ‘수학계의 일반적 승인’이다. 지금까지는 이 과정들이 대체로 한 연구자나 소수 연구팀의 시간 안에서 이어졌다. 연구자가 아이디어를 발견하고 증명을 쓰며 동료들이 읽고 학술지에 출판했다.

AI가 수백 개의 연구결과를 단기간에 생성할 수 있다면 이 순서가 달라진다. 증명의 생산은 매우 빨라질 수 있지만 그 결과가 기존 문헌에서 얼마나 새로운지 조사하고, 핵심 아이디어를 이해하고, 오류를 독립적으로 검증하며, 다른 수학자에게 설명하는 과정은 여전히 많은 시간이 필요하다.

첫 번째 역사인 힐베르트의 23개 문제는 난제의 목적이 단순히 빈칸을 지우는 데 있지 않다는 사실을 보여 준다. 힐베르트가 던진 문제들은 20세기 수학의 연구방향을 움직였고, 일부 문제는 해결 과정에서 애초의 기대와 완전히 다른 이론을 낳았다. 밀레니엄 문제도 같은 전통을 이어 받아 ‘깊은 문제를 향해 가는 과정에서 새로운 수학이 나온다’는 가치를 강조한다.

두 번째인 4색정리는 ‘증명’과 ‘이해’가 항상 같은 속도로 움직이지 않는다는 사실을 처음 크게 드러냈다. 컴퓨터가 엄청난 수의 사례를 검사해 정리의 정확성을 뒷받침할 수 있지만, 인간은 여전히 왜 그런 구조가 필연적인지 더 짧고 개념적인 설명을 원할 수 있다. 오늘날 AI가 만든 거대한 논문을 보며 수학자들이 느끼는 불편함은 이 오래된 논쟁의 확장판이다.

세 번째인 Flyspeck은 그 간극을 줄이는 한 가지 방법을 보여 준다. 증명보조기는 인간이 직접 모든 계산을 반복할 수 없는 경우에도 형식논리를 통해 정확성을 높은 수준으로 검증할 수 있다. AI의 증명 능력이 커질수록 Lean 같은 형식검증의 중요성도 함께 커질 가능성이 높다.

그렇지만 형식검증이 있다고 해서 수학자의 역할이 모두 사라지는 것은 아니다. AI가 내놓은 명제가 원래 연구문제와 정확히 같은지, 선행연구를 어디까지 사용했는지, 이미 알려진 결과보다 무엇이 새로운지, 200쪽의 논증 속 핵심 아이디어를 20쪽 또는 한 문장으로 설명할 수 있는지와 같은 문제는 다른 종류의 판단을 요구한다.

현재 공개된 오픈AI 결과도 같은 원칙으로 읽을 필요가 있다. 예를 들어 ‘준리만 가설’에 관한 결과는 정식 리만 가설의 해결과 구분해야 한다. 오픈AI가 제시한 나비에-스토크스 해법은 클레이수학연구소도 중대한 성과로 평가하고 있지만, 연구소의 규칙상 공식적인 상의 인정에는 출판과 최소 2년의 시간, 세계 수학계의 일반적 승인이 필요하다.

독립 수학·AI 자문그룹이 이번 대규모 공개를 두고 “공개는 시작이지 완료가 아니다”라는 취지로 강조한 이유도 여기에 있다. 저장소에 논문이 올라온 것은 다른 수학자가 읽을 수 있게 됐다는 뜻이지, 수백 개의 결과가 모두 이미 검증되고 기존 수학체계 속의 위치까지 결정됐다는 의미는 아니다.

따라서 앞으로 수학의 연구과정은 AI가 후보 아이디어 생성 → 형식검증으로 논리 확인 → 분야 전문가가 의미와 기존 연구 비교 → 독립적인 재검증 → 학술공동체가 설명과 일반화를 축적하는 방식으로 점점 분업될 수 있다.

이때 수학자의 역할은 문제를 직접 푸는 사람에서 단순히 AI의 답을 채점하는 사람으로 축소된다고만 볼 필요도 없다. 어떤 문제가 중요한지를 고르고, AI가 만든 수많은 결과 가운데 가치 있는 것을 찾아내고, 복잡한 증명에서 새로운 개념을 추출하며, 다음 세대가 이해할 수 있는 형태로 정리하는 일이 오히려 더 중요해질 수 있다.

AI가 바꾸고 있는 것은 ‘증명이 필요한가’가 아니라 증명을 생산하는 속도와 증명을 이해하는 속도 사이의 균형이다. 1900년 힐베르트 시대에는 좋은 문제를 찾고 해결하는 데 수십 년이 걸렸고, 1976년에는 컴퓨터가 인간이 확인하기 어려운 수천 개의 사례를 대신 검사했으며, 2014년에는 증명보조기가 400년 된 난제의 논리를 기계적으로 검증했다. 2026년에는 한 단계 더 나아가 AI 자체가 대량의 새로운 증명을 제안하기 시작했다.

그래서 앞으로 수학에서 가장 값비싼 능력은 정답을 빨리 생산하는 능력 하나가 아닐 수 있다. 무엇이 정말 새로운지 알아보고, 어떤 증명을 믿을 수 있는지 검증하고, 기계가 찾아낸 사실을 인간이 이해할 수 있는 하나의 아이디어로 바꾸는 능력이 수학의 새로운 중심과제가 될 가능성이 있다.

배경지식 참고

• OpenAI, 「Sharing AI progress in mathematics」, 2026년 10월 6일 · 내부 프런티어 모델이 만든 대규모 수학 연구결과의 공개방식과 독립 수학·AI 자문그룹의 권고를 반영한 현재 공개원칙을 확인하기 위한 자료.
• OpenAI Math 공개 저장소, 「Overview」 · 수백 개 결과군의 분야별 구성과 준리만 가설, 힐베르트 10번째 문제의 유리수 버전 등 개별 결과가 실제로 주장하는 명제의 범위를 구분하기 위한 1차 자료.
• OpenAI Math, 「The Quasi-Riemann Hypothesis」 및 Lean formalization notes · 리만 제타함수와 Dirichlet L-함수에 대해 실수부 7/8보다 큰 영역의 무영점 결과를 주장하며 이것이 정식 리만 가설과 다른 명제임을 확인하기 위한 자료.
• OpenAI, 「On the Navier-Stokes Millennium Prize Problem」, 2026년 9월 8일 · 내부 AI 시스템이 나비에-스토크스 문제의 해법을 제시하고 논문과 Lean 형식검증을 공개한 과정과 현재 주장 범위를 확인하기 위한 자료.
• Clay Mathematics Institute, 「Navier-Stokes Announcement」, 2026년 9월 11일 · AI가 제시한 나비에-스토크스 결과를 중요한 잠정적 해결로 평가하면서도 정식 검증절차가 남아 있음을 확인하기 위한 공식 자료.
• Clay Mathematics Institute, 「Rules for the Millennium Prize Problems」 · 제안된 해법이 적격 학술매체에 출판되고 최소 2년이 지나며 세계 수학계의 일반적 승인을 받아야 공식 심사를 진행할 수 있다는 밀레니엄상 검증원칙을 이해하기 위한 자료.
• Clay Mathematics Institute, 「Riemann Hypothesis」 · 정식 리만 가설이 리만 제타함수의 비자명한 모든 영점이 실수부 1/2인 직선에 놓인다는 명제임을 확인하기 위한 공식 문제설명.
• Advisory Group on Mathematics and Artificial Intelligence, 「On OpenAI’s Release of Mathematical Results」, 2026년 10월 6일 · 대규모 AI 수학결과의 공개가 인간의 이해와 수학적 지식으로의 편입과정의 시작이며 자문 자체가 결과를 보증하는 것은 아니라는 입장을 확인하기 위한 자료.
• David Hilbert, 「Mathematical Problems」, 1900 · 파리 국제수학자대회에서 미해결 문제를 통해 새 세기의 수학 발전방향을 제시하고 이후 23개 문제로 출판한 연구의제 설정의 고전적 사례.
• American Mathematical Society, 「A Sideways Look at Hilbert’s Twenty-three Problems of 1900」 · 힐베르트의 23개 문제가 20세기 수학 연구와 문제해결의 명성체계에 미친 영향을 이해하기 위한 역사자료.
• Clay Mathematics Institute, 「The Millennium Prize Problems」 · 2000년 7개 밀레니엄 문제와 문제당 100만달러의 상금이 만들어진 목적, 힐베르트 문제와의 역사적 연결을 이해하기 위한 공식 자료.
• Kenneth Appel·Wolfgang Haken, 「Every Planar Map is Four Colorable」, Bulletin of the American Mathematical Society, 1976 · 4색정리를 전자계산의 실질적 도움으로 처음 증명한 역사적 논문.
• American Mathematical Society, 「The Four Color Theorem」 관련 자료 · Appel-Haken 증명이 1,936개의 구성을 대규모 컴퓨터 계산으로 검사하면서 수학에서 컴퓨터 보조 증명의 정당성 논쟁을 촉발한 배경을 이해하기 위한 자료.
• Georges Gonthier, 「Formal Proof—The Four-Color Theorem」, Notices of the American Mathematical Society, 2008 · Coq 증명보조기를 이용해 4색정리의 수학과 계산을 형식적으로 검증하고 ‘컴퓨터 계산을 어떻게 신뢰할 것인가’라는 문제를 해결한 방법을 이해하기 위한 자료.
• Thomas C. Hales, 「A Proof of the Kepler Conjecture」, Annals of Mathematics, 2005 · 1611년 케플러의 구 포장 추측을 컴퓨터 계산과 수학적 논증의 결합으로 해결한 원 증명의 공식 출판자료.
• Thomas Hales 외, 「A Formal Proof of the Kepler Conjecture」, Forum of Mathematics, Pi, 2017 · HOL Light와 Isabelle을 사용해 케플러 추측의 전체 증명을 형식검증한 Flyspeck 프로젝트의 공식 학술보고.
• Flyspeck Project 자료 · 1998년 컴퓨터 보조 증명 뒤 2003년부터 전체 형식화를 추진하고 2014년 형식증명을 완성한 과정을 통해 ‘컴퓨터 계산의 신뢰’에서 ‘기계적으로 검증된 논리’로 발전한 수학 증명의 역사를 이해하기 위한 자료.

청랑학습코칭 × 청랑북스
역사와 현대 사회의 연결을 살펴보고, 사실과 해석을 구분하며 논술에 활용할 수 있는 배경지식을 전합니다.
청랑학습코칭 · 청랑북스

© 2026 청랑학습코칭 & 청랑북스. All Rights Reserved.