AI는 이제 정리를 증명한다, 하지만 모두를 형식화하는 건 다른 문제
How to Formalize All of Mathematics
OpenAI의 최신 발표 이후 AI의 정리 증명 능력이 주목받으며 모든 수학을 형식화하자는 제안이 나오고 있다. 수학자들은 대규모 형식화가 수학적 탐구를 확장할 수 있다고 보면서도, 속도만 앞세운 무분별한 시도는 자원 낭비를 넘어 지속적인 피해를 줄 수 있다고 경고한다. 이들은 AI 생성 코드를 정리하는 데 드는 수고가 처음부터 제대로 작성하는 것보다 클 수 있다는 경험을 공유하며, 신중하고 협력적인 접근을 촉구한다.
잘 되면 대규모의 협력적 형식화 노력은 수학적 탐구와 발견을 엄청나게 확장할 수 있다. 잘못 되면 기껏해야 자원 낭비에 그치겠지만, 더 가능성이 높은 것은 지속적인 피해를 입히는 것이다.