대학원 시절 지도교수의 연구 수업에서 열린 문제에 직접 기여할 기회가 있었음. 어느 금요일 교수는 참이길 바라는 매끄럽고 아름다운 추측을 제시했지만, 기묘한 예외를 좋아하고 증명 도구도 부족했던 나는 반례를 찾는 데 집중해 한 시간 만에 발견함
교수는 주말 내내 증명에 실패했는데, 서로 다른 도구·기대·동기를 지닌 사람이 같은 문제를 보면 전혀 다른 방향에서 기여할 수 있음을 보여준 일임. 위대한 지도교수에 비할 수는 없었지만, 그때만큼은 다른 방향을 볼 이유가 있었고 그것이 내 유일한 수학 연구 기여인 작은 반례로 이어짐

기계가 반례를 잘 찾는 이유도 여기에 있을 듯함. 추측에 대한 미적 집착도 없고 추한 결과를 내놓는 데 부끄러움도 없음

수학자로서 내 체감은 반대임. 증명은 아는 증명을 조금 변형하면 되지만, 반례를 만들려면 대상의 구조를 깊이 이해해야 해서 내 능력을 넘어설 때가 많음
다만 이는 내가 이해하기 어려운 추상적 대상을 주로 다루기 때문일 수 있고, 수나 다항식에서는 반대일 가능성이 큼

학생에게 아직 풀지 못한 문제를 공개하고 참여를 권하는 교수·연구자·교사는 더 높이 평가받아야 함. 대학 첫 공학 수업에서 강사가 1학년들에게 “우리가 아직 풀지 못한 문제들이니 아이디어가 생기면 알려 달라”고 했을 때 어느 때보다 환영받고 공동체에 포함된 느낌이었고, 자칫 따분할 수 있는 학업 초반에 큰 영감을 줬음

쌍둥이 소수 추측으로 유명한 Yitang Zhang은 Purdue에서 Tzuong-Tsieng Moh의 지도를 받으며 야코비안 추측을 7년간 연구함. 학위논문의 핵심 단계가 Moh의 잘못된 따름정리에 의존한 것으로 드러났고, Moh는 추천서 작성을 거부했으며 Zhang은 교육·연구직을 구하지 못해 수년간 Subway에서 일하게 됨
1986년 연구를 시작할 때 ChatGPT가 있었다면 어땠을지 궁금함. 지금은 감동적인 성공담이 됐지만, “庾信平生最萧瑟，暮年诗赋动江关”이라는 시구처럼 복잡한 감정을 불러일으킴

수학 박사학위 발표 중 심사 교수가 증명의 결함을 발견한 적이 있음. 학생이 이해한 뒤 “이제 어떻게 하죠?”라고 묻자 심사 교수는 그저 어깨를 으쓱했음

훗날 쌍둥이 소수 추측에서 성공했으니 감동적이라고 할 수는 있겠지만, 학계의 이런 이야기에 지쳤음. 정치와 평판 관리가 지나치게 많고 Zhang은 그런 고통을 겪지 말았어야 함
수학 쪽으로 연구를 넓히며 문헌 속 명제 중 상당수가 거짓이고 응용 문헌에까지 광범위하게 전파됐다는 데 놀랐음. 문제를 알려도 Zhang의 일화처럼 방어와 부정으로 대응하는 경우가 많음. LLM은 증명에 유용하지만 크게 틀리기도 하며, 다른 직관으로 탐색 방향을 제안하는 또 한 사람과 비슷해서 1986년에도 결과는 같았을 듯함

ChatGPT가 옮긴 시의 뜻은 “Yu Xin의 삶은 철저히 쓸쓸했으나, 노년의 시와 부가 강호를 뒤흔들었다” 정도임

이는 축구 팬처럼 수학을 경쟁으로 보는 건강하지 못한 관점임. 수학에서 가장 가치 있는 것은 아름다운 증명만이 아니라 유용한 정의이며, 좋은 정의와 그로부터 좋은 추측을 만드는 일은 LLM이 아직 정복하려 하지 않은 영역임

아직 그렇게 극적이지는 않지만 곧 그 단계에 이를 가능성은 있음. AI 능력이 점근적으로 발전할지 가속할지 구조적으로 예측할 근거가 없고, 어떤 문제가 새 방법에 풀릴지도 양쪽 가능성이 모두 열려 있음
AI 능력의 내부와 성장 곡선을 이해하지 못하며, 의도적으로 성능을 낮춰 보이는지조차 정확히 알 수 없음. 측정에 저항하는 창발 현상일 수도, 몇 년 뒤 시계처럼 예측 가능해질 수도 있음. 아는 사람은 없고, 있다면 말하지 않으며 목소리 큰 사람들도 아는 게 없음

대학원생의 의미 있는 성과를 크게 앞당긴다면 학생당 연 $2,400을 투자하지 않을 이유가 없음. 전체 비용에서 보면 푼돈에 가까움

일부 대학원생은 자신을 “의미 있는 결과를 생산하는 기계”가 아니라 윤리적 존재로 봄. 유용한 LLM도 도용된 학습 데이터와 막대한 환경 영향 때문에 정당화하기 어렵다는 점을 모두 알고 있음

EPSRC 박사과정의 생활비 장학금은 약 £20,000이므로 연간 비용의 약 10%에 해당함. 학생 개인에게는 큰 부담임

대학 시절 LLM이 만든 Lean 형식화가 있었다면 좋았을 것임. 강의 슬라이드의 수학에는 오류가 많았고, 일부 교수는 “증명은 슬라이드에 있다”며 해명 요구를 거절하면서도 오류를 인정하는 데 인색했음
Lean 증명 자체는 이해에 적합하지 않은 경우가 많지만, 이를 바탕으로 사람이 이해하기 쉬운 논증을 생성할 수 있기를 바람

첫 주장에는 동의하기 어려움. 학습 곡선은 가파르지만 잘 작성된 Lean·Agda·Rocq 형식화는 증명을 이해하는 데 탁월함. 좋은 형식화는 개요와 핵심 논증을 구조적으로 보여주고, 종이 증명과 달리 원하는 깊이까지 모든 단계의 세부 사항을 확인하게 해줌
Martín Escardó의 TypeTopology Agda 저장소가 좋은 예임. 반면 현재 LLM이 생성한 형식화는 매우 난잡할 수 있어 참을 인증하고 흥미로운 논증을 담더라도 수학적 이해를 높이는 형태로 다듬는 데 상당한 작업이 필요함. 대화형 Agda 튜토리얼은 lets-play-agda.quasicoherent.io에 있음

형식화는 논쟁을 끝내고 의심을 완전히 제거하는 Leibniz식 접근에도 쓸 수 있음

수학자에게 반례는 물리과학의 예상 밖 결과처럼 당장은 성가셔도 모델의 부정확성을 드러내 엄청나게 중요할 수 있는 것인지, 아니면 프로그래밍의 버그 보고처럼 사소하고 귀찮은 세부 사항인지 궁금함

반례는 조건의 역할을 명확히 해줌. 증명의 각 조건을 위반했을 때 무엇이 실패하는지 보여주는 가장 단순하고 기억하기 쉬운 반례가 있으면 매우 유용함
수학자들은 머릿속에 반례 동물원을 가지고 다니는 경향이 있음. 정리를 복원할 때도 날카롭고 기억에 남는 반례를 떠올리며 그것들을 배제하도록 정의역과 조건을 좁힐 수 있음

《Counterexamples in Topology》와 《Counterexamples in Analysis》처럼 반례를 통해 분야의 미묘한 차이를 가르치는 교육서가 있음. 의도된 정상적 대상만 배우는 것보다 병리적·퇴화한 예시에서 세부 사항을 익히기 쉬워 인기가 많음

이 수학의 상당 부분은 이해하기 어렵지만 대체로 정리 증명을 다루는 듯함. AI 수학이 계속 가속하면 장차 공학이나 생의학에 응용될 새로운 수학까지 발견할지, 인류의 거대한 돌파구 직전인지, 아니면 이미 알려진 것을 증명하는 데 그칠지 궁금함