Mathematics in the age of AI

1. 역사적 서론

• 수학자들은 수 세기 동안 소박한 기초 체계 아래서 성공적으로 연구하며, 수학적 대상과 증명의 정확한 정의는 대체로 철학자들에게 맡겨 두었다.집합, 수, 무한이 무엇인지 명시적으로 규정하지 않은 채 이들에 관한 정리를 증명했다.출처: §1 · p. 1
• 러셀의 역설 과 괴델의 불완전성 정리 는 수학자들이 그동안 암묵적으로 받아들였던 기초 가정을 재검토하게 했다.소박한 집합론에는 모순이 있었고, 형식 체계는 무모순성과 충분한 표현력을 갖추면서 동시에 자신의 무모순성을 증명할 수는 없었다.출처: §1 · p. 1
• 기초론의 위기는 대상과 추론 규칙을 검토하고 가르치며 기계화할 수 있는 명시적이고 엄밀하며 표준화된 체계를 낳았다.기초론 연구는 계속되고 있지만, 이 체계는 한 세기에 걸친 엄격한 검증을 견뎌 내며 수학에 신뢰할 수 있는 연구 환경을 제공한다.출처: §1 · p. 1
• 저자는 이제 수학이 가치와 관행을 둘러싼 격변에 직면해 있으며, 기여, 보상, 이해, 공로 귀속에 관한 명시적인 목표가 필요하다고 주장한다.저자는 이러한 목표를 검토하고 명문화하는 과정이 수학계를 더 강하고 변화에 잘 견디는 공동체로 만들 것으로 기대한다.출처: §1 · pp. 1–2

• 핵심 질문은 오늘날의 AI 기술과 그 기술이 실제로 갖추었거나 갖추었다고 주장되는 수학 과제 수행 능력에 수학계가 어떻게 대응해야 하는가이다.저자는 이를 ‘공동체 대응 질문’이라 부른다.출처: §2 · p. 2
• 이 질문은 수학계 전체가 다뤄야 한다. 누구도 모든 답을 갖고 있지 않으며, 저자는 접근 방향을 제시한다.출처: §2 · p. 2
• 대응에 관한 질문은 수학적이라기보다 메타수학적·정치적·윤리적·사회학적·문화적 질문이며, 순수한 논리적 논증만으로는 결론을 낼 수 없다.그럼에도 저자는 질문의 구조를 명확히 하기 위해 추측과 가설을 비롯한 수학적 언어를 빌려 쓴다.출처: §2 · p. 2

3. 첫 번째 하위 질문: AI의 능력

• AI 능력 추측은 도구, 비용, 감독, 과제, 분야, 성공률, 정확성, 질을 포괄하는 매개변수를 통해 가까운 미래의 연구 수준 수학 능력을 기술한다.이 미정 항목들을 어떻게 정하느냐에 따라 서로 다른 수많은 추측이 정의된다. 이 글에서는 약한 형태와 강한 형태만 대략적으로 구분한다.출처: §3 · p. 2
• 약한 추측조차 성립하지 않는다면 기존 방식의 유지에 힘이 실린다. 반면 가장 강한 형태가 성립한다면 수학 연구 관행, 특히 미해결 문제의 풀이를 우선시하는 관행을 그대로 유지하기 어려워진다.약한 추측이 성립하지 않는 경우 중요성을 낮게 평가하게 되는 대상은 현세대 AI 도구와 그것이 수학 연구에 갖는 장기적 의의다.출처: §3 · p. 2
• AI 능력에 대한 견해차는 수학계의 대응에 관한 건설적 논의를 가로막지만, 이 글은 그 논쟁의 시비를 가리기보다 의도적으로 논외에 둔다.그와 달리 AI와 수학에 관한 공개 논쟁은 대부분 어떤 능력 추측이 참인지에 초점을 맞춰 왔다.출처: §3 · pp. 2–3
• 공개된 근거에는 과학적 통제가 부족한 경우가 많으며, 보고 편향, 비과학적 유인, 비공개 변수, 능력에 관한 주장과 그 능력의 바람직함을 혼동하는 문제가 있다.시도 횟수, 인간의 보조, 연산 자원 사용량, 기존 문헌에 의한 오염 등은 공개되지 않는 경우가 많다. 성공은 널리 알려지는 반면 실패는 그렇지 않다.출처: §3 · p. 3
• First Proof의 두 번째 문제 묶음 [6]에서는 통제된 조건에서 연구 수준 수학 문제 10개 중 7개에 대해 AI 시스템 4개 중 하나 이상이 합격 판정을 받았다.First Proof 는 문제 제공자가 해답을 알고 있지만 온라인 어디에도 게시된 적 없는 문제를 사용한다. 모델은 May 28, 2026 기준으로 일반에 공개되어 있었으며, 전문가들이 정확성과 서술을 검토했다. 합격한 풀이는 사실상 흠이 없거나 경미한 수정만 필요하다고 평가되었으며, 연산 비용은 문제당 수십~수백 달러 수준이었다.출처: §3 · p. 3

4. 역량 추측의 여공간

• 이 글은 Question 2.1에서 AI 역량 추측의 ‘직교여공간’이라 부르는 부분을 분리해 다룬다.작업 가설을 채택하면 이 부분을 AI의 역량에 관한 문제와 분리할 수 있다.출처: §4 · p. 3
• 작업 가설은 AI가 비교적 가까운 시일 안에 연구 수준의 수학 과제 중 적정한 비율을 적정한 성공률, 품질, 감독 수준, 비용으로 수행하게 된다고 가정한다.‘적정하다’는 말의 정확한 의미는 이 분석에서 중요하지 않다.출처: §4 · p. 3
• 이 분석은 작업 가설을 가정하되, 독자에게 그 실현을 바라거나 이를 믿거나 참으로 받아들이라고 요구하지 않는다.가설을 뒷받침하거나 반박하는 증거는 이후 논의와 별개의 문제다.출처: §4 · p. 3

• 수학 공동체는 공표한 목적뿐 아니라 실제로 최적화하는 암묵적 목표도 파악해야 한다.이는 수학 공동체와 수학 연구 모두의 목표, 목적, 가치에 관한 질문이다.출처: §5 · p. 3
• 작업 가설 아래에서 수학자들은 더 이상 자신의 목표에 대한 성찰을 인문학에 맡길 수 없지만, 이러한 성찰은 그 가설과 무관하게 가치가 있다.역사적으로 수학자들은 기술적 작업에 집중하면서 이러한 질문을 대체로 역사가, 철학자, 사회학자에게 맡겨 왔다.출처: §5 · p. 4
• 수학의 목표에는 문제 해결, 이론·구조·기법 개발, 세계 이해, 공동체 유지, 후학 양성, 공동 지식 축적, 오래도록 미적 가치를 지니는 작품 창조가 포함된다.저자는 이를 일부만 나열한 목록으로 제시하며 독자들에게 더 보태기를 권한다.출처: §5 · p. 4
• 생성형 시스템은 실질적 속성보다 외견상의 충족도를 최적화하고, 산업계의 유인 구조는 입증하고 인용하며 벤치마크로 평가할 수 있는 성과에 보상하므로, AI는 대리 지표의 신뢰성을 위협한다.이는 굿하트의 법칙을 보여 준다. 굿하트의 통화정책에 관한 관찰 을 잇는 스트래선의 정식화 에 따르면, 측정치를 목표로 삼으면 그 신뢰성이 훼손된다.출처: §5 · pp. 4–5
• 수학의 한두 가지 목표에 대한 과도한 최적화는 이전에 조화를 이루던 목표들이 서로 어긋나게 할 수 있다.역사적으로 한 목표를 향한 진전은 대개 다른 목표들도 진전시켰기에, 일부 목표를 편리한 대리 지표로 삼을 수 있었다.출처: §5 · pp. 4–5

• 해결한 문제 수를 극대화하려면 정확성 검증이 필요하다. AI와 증명 보조기 언어로의 자동 형식화 는 증명 생성과 검증을 모두 가속한다.해답 수만 세면 틀린 해답의 제출을 부추긴다. 형식 검증은 저자의 평판이나 성실성과 무관하게 정확성을 보장하며, 작업 가설은 이러한 가속이 계속될 것으로 예측한다.출처: §6 · pp. 5–6
• 올바른 증명에는 이해 가능성도 필요하다. 현재 AI의 설명은 문법과 형식이 거의 완벽해도 새로운 단계를 불분명하게 서술하고 관련 문헌의 맥락이나 전체적인 개요를 빠뜨릴 수 있다.검증된 증명이라도 이를 설명할 수 있는 사람이 없을 수 있다. Erdős 문제 데이터베이스 에 제출된 AI 생성 해답 중에는 이미 전문가의 검증이나 지지를 받지 못한 사례가 있다.출처: §6 · p. 6
• 설명을 지나치게 다듬으면 난이도 단서가 사라져 증명을 읽기는 쉬워도 배우기는 어려워지고 암묵지의 전수도 약해질 수 있다.세심하게 구성한 보조정리, 표기 변경, 드러나는 수정 흔적은 독자가 어디서 천천히 읽어야 하는지 알려줄 수 있다. 이런 단서를 없애는 일은 오탈자, 어색한 표현, 무질서한 구성을 바로잡는 일과 다르다.출처: §6 · p. 7
• 공동체의 수용에는 인간의 느린 소화와 평가가 필요하다. AI를 통한 선별은 전문가의 주의력을 아낄 수 있지만 공동체의 수용이나 인간 심사자를 대신할 수는 없다.저자는 통찰과 실패한 시도를 공유해 이 과정을 도울 수 있지만, 현재 AI의 문제 해결 과정은 여전히 불투명하다. 기여를 충분히 인정받지 못하는 편집과 심사 작업은 개인의 성취를 공동의 진전으로 바꾼다.출처: §6 · p. 8
• 정전화는 폭넓은 합의를 통해 결과를 표준 참고 문헌에 편입하는 과정이다. 저자는 이를 가장 느리고, AI로 최적화하기 가장 어려우며, 가장 가치 있는 단계로 본다.결과는 자연스러운 일반성, 적절한 증명, 다른 결과와의 연결을 갖춘 뒤 표준 도구로 자리 잡는다. 이러한 소화 과정은 다양한 응용을 가능하게 하며, 정전화된 이론은 AI 학습 데이터를 제공한다.출처: §6 · pp. 8–9
• 제안된 최종 목표는 문제 해결, 정확성 검증, 명확한 전달, 공동체의 수용 확보, 해당 분야의 정립된 이론으로의 결과 편입을 결합한다.문제 해결을 세부 과정으로 나누면 암묵적인 하위 목표가 드러난다. 이 사례 연구가 이론 구축, 교육, 지도, 공동체 봉사에 대한 별도의 분석을 대신하지는 않는다.출처: §6 · pp. 5, 9

7. 증명의 희소성과 풍요

• 증명의 풍요는 희소성을 전제로 설계된 수학계의 제도에 부담을 줄 것이다.여기에는 학술지, 연구 우선권에 관한 관행, 채용과 승진 기준, 상, 그리고 연구 프로그램이라는 개념 자체가 포함된다.출처: §7 · p. 9
• 적절한 정책적·문화적 변화가 없으면 검증, 읽기 쉬운 서술 작성, 전문가의 자발적 동료 심사, 정본을 마련하려는 공동체의 노력이 AI의 증명 생성 속도를 따라가지 못할 것이다.정확하고 잘 쓰인 증명조차 전통적인 동료 심사로는 감당하기 어려워질 것이며, 출판만으로는 그 증명이 정본에 통합되리라는 보장이 없다.출처: §7 · p. 9
• AI는 문헌의 증가, 주요 증명의 장문화와 전문화, 이미 과부하가 걸린 심사 체계 등 기존의 부담을 크게 가중할 것이다.이러한 압박은 현대 AI에서 비롯된 것이 아니라 그 이전부터 존재했다.출처: §7 · p. 10

8. 목표에서 권고로

• 저자는 동료들의 비판을 피하려고 자동화 도구 사용을 숨기기보다 투명하게 공개해야 한다.논문에는 도구와 계산 자원 사용을 공개하는 절을 포함해야 한다. 심사자는 출판사의 지침을 따르고, 허용된 AI 사용을 공개하며, 중요한 권고에 책임을 져야 한다.출처: §8 · p. 10
• 저자는 사용한 도구를 공개하고, 정확하고 완전한 참고문헌을 제시하며, 가능하고 적절한 경우 형식 증명을 제공하여 AI가 가중할 수 있는 심사 부담을 줄여야 한다.출처: §8 · p. 10
• 수학계는 증명을 만들어 내고 최초가 되는 데 두는 비중을 줄이고, 해설·심사·출판·정전화 등 증명을 소화하는 과정에 더 큰 비중을 두어야 한다.Bessis 도 마찬가지로 증명 생산을 주된 기반으로 삼는 정리 경제에서 벗어나야 한다고 주장한다.출처: §8 · p. 10
• AI는 수학적 성과를 뒷받침하는 인간의 집단적 노동을 대체하지 않으므로, 공로와 책임은 자동화 시스템이 아닌 인간에게 귀속되어야 한다.출처: §8 · p. 11
• 자동화 도구는 출처를 명시하는 데 한계가 있으므로, 저자는 출처를 적극적으로 찾아 그 공로를 인정하고, 출처를 충분히 밝힐 수 없을 때는 이를 명시적으로 인정해야 한다.출처: §8 · p. 11
• 저자가 결과를 정확하고 전문적으로, 출처를 적절히 밝히며 설명할 수 있음을 설득력 있게 입증하지 못한다면 그 결과를 출판해서는 안 된다.어떤 인간도 제대로 설명할 수 없는 증명은 형식적으로 검증되었더라도 불완전한 것으로 보아야 한다.출처: §8 · p. 11

9. 맺음말

• 문제 해결의 목표와 가치에 대한 분석을 교육, 지도, 채용, 연구비 신청, 논문 심사, 대중 소통으로 확장해야 한다.작업 가설은 수학 활동의 이 모든 측면에 영향을 미칠 수 있다.출처: §9 · p. 11
• 교육과 젊은 수학자 양성에서는 인간만이 할 수 있는 일을 강조하고 AI 사용을 엄격히 제한해야 한다.과제의 정답을 내는 것만으로는 수학자를 양성한다는 목표를 달성할 수 없다.출처: §9 · p. 11
• 다른 영역에서는 수학자들이 공급업체가 아닌 자신들의 기준에 따라 모범적인 AI 활용 방식을 정하고, 상호 보완적인 작업 절차와 기반 시설을 개발해야 한다.공동 형식화 프로젝트, 구조화된 문제 데이터베이스, 해설과 부정적 결과 또는 부분적 결과를 발표할 새로운 장이 그 예다.출처: §9 · p. 11
• 수학 공동체는 AI의 능력과 자신들의 목표와 가치를 모두 공개적으로 논의해야 한다.이 글은 이 제안을 라이덴 선언과 연결한다.출처: §9 · p. 11
• 수학자들은 내실 있는 과학 보도를 지원하고 AI를 활용한 결과의 맥락을 대중에게 설명해야 하며, 특히 그 깊이와 난도, 의의를 평가하는 데 세부 분야의 전문성이 필요한 경우에는 더욱 그렇다.또한 비슷한 어려움에 직면한 다른 연구자와 창작 분야 종사자들과 협력하고 이들을 지원할 기회를 찾아야 한다.출처: §9 · p. 11

• Mathlib [12]는 통합된 형식화 수학 라이브러리를 제공한다.출처: Appendix A · p. 12
• 열거된 데이터베이스에는 에르되시 문제 데이터베이스 와 최적화 상수 데이터베이스 가 포함된다.출처: Appendix A · p. 12
• Palomar는 형식화된 증명 등록부로 소개된다.출처: Appendix A · p. 12
• Mathematical Discourse [4]는 연구 발표를 다루는 동료 심사 영상 학술지다.출처: Appendix A · p. 12
• SAIR 재단의 수학 경진대회 도 새로운 기반 시설의 사례로 제시된다.출처: Appendix A · p. 12
• First Proof 프로젝트 [7]도 기반 시설의 사례에 포함된다.출처: Appendix A · p. 12