AI가 수학자들을 반례의 홍수 속으로 밀어넣다

Human mathematicians are being outcounterexampled

케빈 버자드(Kevin Buzzard)는 AI가 수학의 난제들에 대한 반례를 연이어 발견하는 최근 상황을 정리한다. ChatGPT가 Erdős의 단위 거리 추측을 반증한 데 이어, OpenAI의 Sol이 해당 증명을 완전히 형식화했고, Logical Intelligence의 시스템도 자동 형식화에 성공했다. 또한 Grothendieck의 60년 된 문제인 유한 평탄 군 스킴의 차수에 대한 반례가 발견되었고, Jacobian 추측에 대한 반례도 제기되었다. 버자드는 이러한 사건들이 인간 수학자들의 역할과 증명의 신뢰성에 대한 근본적인 질문을 던진다고 논한다.