수학자들, 상하이 AI Lab 'Intern-S2'와 협업해 1995년 Ghys 추측의 3차원 경우 증명…Lean으로 검증(보도)

확인된 내용 (사실)

Pandaily에 따르면 수학자들이 상하이 AI Lab의 모델 Intern-S2와 여러 차례 대화를 주고받으며 Étienne Ghys가 1995년에 낸 추측 가운데 여차원(codimension) 1인 경우의 증명을 만들었다. 이후 베이징대 팀이 이 증명을 정리 증명 언어 Lean으로 형식화해 검증했다.

의미 (해석)

AI가 답을 혼자 내놓은 사례가 아니다. 사람과 여러 번 대화하며 증명을 만들고 Lean으로 형식 검증까지 마친 사례다. 최근 AI가 낸 수학 결과의 신뢰성 논란 속에서 검증 가능한 협업 방식의 예가 된다.

출처

• 보도 Mathematicians Use Shanghai AI Lab's Intern-S2 to Prove 3D Ghys Conjecture, Verified in Lean Pandaily