AI 수학 연구

ChatGPT·Claude·Gemini 같은 LLM과 추론 모델을 수학 연구 도구로 쓰는 흐름으로, 문헌 탐색과 예시·반례 찾기부터 대략적인 스케치를 엄밀한 증명으로 풀어 쓰고 형식 검증하는 단계까지 돕는다. 다만 결과를 확인하고 책임지는 쪽은 사람이다.

내가 따라갈 수 있는 만큼만 맡긴다

MIT 에팅오프 교수가 학생에게 주는 핵심 원칙은 "AI와 나눈 수학을 내가 계속 따라잡고 있어야 한다"는 것이다. 이해하지 못한 증명을 그대로 가져오면 연구가 오히려 망가진다.

실제로는 이렇게 나눠 쓴다. 막혔을 때는 비슷한 문제가 다른 분야에 있었는지 물어 문헌 탐색 시간을 줄이고, 추측을 세웠으면 작은 경우의 예시와 반례를 먼저 뽑아 달라고 한다. 지루한 대수 계산은 컴퓨터 대수 시스템과 함께 돌리게 하고, 결과는 직접 한 줄씩 확인한다.

검산은 Lean과 사람이 맡는다

AI의 증명은 그럴듯하지만 틀릴 수 있다. 그래서 Lean 같은 증명 검사기에 형식화해 넣으면 각 단계가 맞는지 기계가 확인해 준다. 테렌스 타오는 이 덕분에 큰 증명을 여러 사람(또는 AI)이 나눠 맡아도 서로 믿을 수 있게 됐다고 본다.

성과만큼 논란도 커졌다

범용 추론 모델이 80년 된 에르되시 단위거리 추측을 반증했지만, 최초 증명은 이후 사람 수학자들이 크게 다듬었다. 한 회사가 AI 수학 원고 수백 편을 한꺼번에 공개했다가 하루 만에 오류가 있는 원고를 철회한 일도 있었다.

그래서 학계는 사용 지침을 만들고 있다. 논문에 AI를 쓴다면 주요 기여를 밝히고, 공저자 동의와 학술지·기관 규정을 지키며, 미공개 아이디어를 넣을 때 개인정보 규칙도 확인해야 한다.

막힌 곳을 뚫고 검산하는 데 주로 쓴다

가장 흔한 건 연구하다 막힌 지점에서 대화 상대로 쓰는 방식이다. 비슷한 결과가 다른 분야에 있는지 묻고 예시를 뽑게 한 뒤, 나온 증명은 직접 읽거나 Lean으로 확인한 것만 받아들인다.