기타 Hacker News · 4시간 전

수학 노베이스 개발자가 AI로 50년 묵은 난제 푼 썰.txt

핵심 요약
  • 수학을 잘 모르는 개발자가 클로드와 한 달 동안 방대한 양의 토큰을 소모하며 50년 된 콘웨이의 수학 추론을 증명해냈다고 밝혔습니다.
  • 내용을 깊이 이해하지 못한 채로 AI를 활용해 정형 증명 언어(Lean) 코드를 완성하고 기계적 검증까지 통과한 독특한 사례입니다.
  • 수학자들의 공식 동료 평가는 아직 받지 않았으나 기계적 검증 통과 및 전문가들의 긍정적 검토를 바탕으로 반박과 검증을 환영하고 있습니다.
요약 최근 AI를 활용한 수학적 돌파구가 화제가 되는 가운데, 수학을 잘 모르는 비전문가가 클로드(Claude)와 대량의 토큰, 그리고 한 달간의 여가 시간을 쏟아부어 유명 수학자 존 콘웨이(John Conway)의 50년 된 추론을 증명해냈다는 글이 올라와 해외 커뮤니티에서 큰 주목을 받고 있습니다. 작성자는 수학적 본질을 다 이해하지 못해도 최첨단 모델을 이용해 미해결 문제를 '바이브 코딩'하듯 풀어보고 싶다는 호기심에서 프로젝트를 시작했다고 밝혔습니다. 그는 클로드에게 모든 무한대와 무한소 등을 포함하는 수학 체계인 '초현실수(Surreal Numbers)' 분야의 미해결 문제를 추천해달라고 요청했고, 클로드는 콘웨이의 책 발표 50주년이 되는 해라는 점과 함께 '콘웨이의 세분화 추론(Conway's refinement conjecture)'을 추천했습니다. 이 문제는 전정수(omnific integers)에 대해 ab = cd일 때 이를 공통 조각들로 분해 및 재조합할 수 있다는 성질을 다룹니다. 작성자는 정형 증명 언어인 린(Lean)을 활용해 증명을 작성했으며, 비록 전문 수학자들의 공식적인 동료 평가를 거치지는 않았지만 팔로마 레지스트리(Palomar registry)의 기계적 검증을 통과했다고 설명했습니다. 또한 린과 관련 분야 전문가들로부터 명제가 타당해 보인다는 의견을 받았으며, 혹시 모를 반박이나 검증을 환영한다고 덧붙였습니다. 수포자에 가까운 개발자가 AI와의 집요한 대화만으로 난해한 정수론 추론의 정형 검증을 시도해 통과시켰다는 소식에 많은 네티즌들이 놀라워하고 있습니다.
Sponsored · 광고