AI가 수학자를 이겼다, 이번엔 '반례 찾기'로

임페리얼칼리지 수학자이자 Lean 형식화의 대가 케빈 버저드가 흥미로운 전환을 짚는다. 그동안 화두는 'AI가 정리를 증명할 수 있는가'였지만, 더 빠르게 현실이 된 능력은 정반대다. 바로 '반례 찾기'. 수학자들은 그럴듯해 보이는 명제나 보조정리를 참이라 믿고 적어두지만, 상당수는 미묘하게 틀려 있다. 최근 LLM은 이런 거짓 명제에 대해 인간보다 빠르게 구체적인 반례를 제시하며 오류를 잡아낸다. 형식화 작업에서 이 능력의 실용적 가치는 크다. 완전한 증명 자동화는 여전히 어렵지만, '틀렸음을 보여주는' 반증에서는 AI가 이미 인간을 앞지르기 시작했다는 것이 요지다. 즉 AI는 만능 증명기가 아니라, 사람이 놓친 실수를 잡아내는 조력자로서 연구 현장에 스며들고 있다. 검증과 오류 탐지가 중요한 소프트웨어 개발자·연구자에게도, '증명'보다 '반증'에서 먼저 무너지는 지점을 AI가 메운다는 통찰은 곱씹을 만하다.