▲

에르되시 문제 #728, AI가 거의 자율적으로 해결

 (mathstodon.xyz)
1P by GN⁺ 16시간전 | ★ favorite | 댓글 1개
  • 에르되시 문제 #728이 최근 AI 도구에 의해 거의 자율적으로 해결되며 수학 연구 자동화의 새로운 이정표를 세움
  • 문제는 원래 Erdős, Graham, Ruzsa, Strauss가 1975년에 제기한 이항계수의 소인수분해 관련 질문으로, 애매한 조건 때문에 오랫동안 명확히 다뤄지지 않았음
  • ChatGPT가 조정된 제약 조건하에서 증명을 생성하고, Aristotle이 이를 Lean 형식 증명으로 공식화하며 오류를 자동 수정함
  • 이후 여러 참가자들이 ChatGPT를 이용해 자연어로 재작성하고, 문헌 연결과 서사 구조를 강화한 버전을 반복적으로 개선함
  • Terence Tao는 이 과정을 통해 AI의 신속한 증명 작성·수정 능력이 연구 논문 작성 방식 자체를 변화시킬 잠재력을 보여준다고 평가함

AI가 해결한 에르되시 문제 #728

  • 최근 AI 도구의 적용이 에르되시 문제 해결에 새로운 진전을 보였으며, 문제 #728이 거의 자율적으로 AI에 의해 해결됨
    • 초기 시도 후 피드백을 반영해 수정된 버전에서 성공
    • 결과는 기존 문헌에서 동일하게 재현되지 않았으며, 유사한 방법의 비슷한 결과만 존재
  • 이 사례는 최근 몇 달간 AI의 수학적 문제 해결 능력이 실제로 향상되었음을 보여줌
    • 과거에도 AI가 에르되시 문제를 해결한 사례가 있었으나, 대부분은 이후 문헌에서 이미 존재하는 해로 판명됨
  • 이번 문제는 원래 에르되시의 서술이 잘못된 형태로 제시되어 있었고, 최근에야 의도된 형태로 재구성됨
    • 이로 인해 기존 문헌에 관련 연구가 부족했던 것으로 설명됨

문제의 역사와 초기 접근

  • 1975년 Erdős, Graham, Ruzsa, Strauss가 이항계수 (2n choose n) 의 소인수분해를 연구하며 여러 관련 문제를 제시
    • 그중 하나가 a!b! | n!(a+b−n)! 조건과 a+b > n + C log n을 만족하는 무한한 a, b, n의 존재 여부를 묻는 문제였음
    • 그러나 C의 크기(작은지 큰지) 등 여러 부분이 불명확하게 서술됨
  • 몇 달 전 AlphaProof 팀이 문제의 단순 해를 발견했으나, 이는 의도된 문제 정신에 맞지 않아 a,b ≤ (1−ε)n 제약을 추가함
    • 이후 AI 보조 문헌 검색에서도 관련 연구는 거의 발견되지 않음

ChatGPT와 Aristotle의 협업

  • 1월 4일 ChatGPT가 조정된 제약 조건에서 작은 C의 경우에 대한 증명을 생성
    • 이 증명은 Aristotle에 의해 Lean 형식 증명으로 공식화됨
    • 이후 원문을 재검토한 결과, 원래 논문이 이미 작은 C의 경우를 다루고 있었음이 확인됨
  • 다른 참가자가 Lean 증명을 ChatGPT로 자연어로 변환하고, 추가 대화를 통해 개선된 버전을 작성
    • 이 버전은 일부 증명 공백을 메웠으나, 여전히 AI 특유의 어색한 문체와 문헌 인용 부족이 남음
    • 그럼에도 핵심 아이디어를 이해할 수 있을 정도로 읽기 가능한 수준에 도달함

대규모 재작성과 개선된 결과물

  • 추가 프롬프트를 통해 ChatGPT가 큰 C의 경우까지 확장된 증명을 생성
    • 일부 오류가 있었으나 Aristotle이 자동으로 수정하고 Lean 검증된 증명을 완성
  • 세 번째 참가자가 Lean 증명을 압축한 뒤, 다른 참가자가 ChatGPT와 장시간 대화를 통해
    • 문헌 연결과 서사 구조를 강화한 완성도 높은 논문 형태로 재작성
    • 결과물은 AI 생성물의 느낌이 줄어든, 연구 논문 수준에 근접한 품질로 평가됨
    • Tao는 이 텍스트를 에르되시 문제 포럼에서 검토했다고 언급

AI가 바꾸는 연구 논문 작성 방식

  • Tao는 최종 논문은 여전히 핵심 부분은 인간이 작성해야 한다고 보지만,
    • AI와 Lean의 결합이 증명 작성과 수정의 속도를 획기적으로 높였다고 평가
  • 기존에는 논문 한 편을 읽기 좋게 만드는 데 많은 시간이 들고,
    • 심사자 피드백에 따른 수정도 국소적 변경에 그치는 경우가 많았음
  • 그러나 이제는 AI의 텍스트 생성·수정 능력과 형식 증명 도구의 검증 기능이 결합되어
    • 다양한 수준의 정밀도와 서술로 빠르게 새로운 버전의 논문을 생성할 수 있음
  • 하나의 “공식 논문” 외에도, AI가 생성한 다수의 보조 버전이 존재해
    • 다양한 관점과 추가적 가치를 제공할 수 있는 가능성이 제시됨

커뮤니티 반응

  • 일부 사용자는 AI가 생성한 문서의 추가적 가치를 “다른 각도에서 볼 수 있는 능력”으로 설명
  • 다른 수학자들은 AI 결과의 독창성 측정이나 기존 문헌과의 유사성 평가의 필요성을 제기
    • 예를 들어, Lean 형식 증명 길이 비교를 통한 정량적 유사성 측정 제안
  • 또 다른 논평에서는 AI가 코드 리팩터링처럼 논문을 전역적으로 재작성할 수 있어
    • 연구자들이 더 높은 수준의 문서 구조 설계에 집중해야 한다는 의견도 제시됨
  • 일부는 AI가 수학자의 역할을 대체할 가능성에 회의적 반응을 보였으나,
    • 다른 이들은 이를 협업과 사고 확장의 새로운 기회로 평가함
▲
GN⁺ 16시간전  [-]
Hacker News 의견들

  • 나는 Harmonic에서 일하고 있으며, 우리가 만든 Aristotle에 대해 몇 가지 오해를 바로잡고 싶음
    Aristotle은 최신 AI 기법을 적극적으로 활용하며, 언어 모델링도 포함함
    영어로 된 비공식 증명을 입력하면, 그 증명이 맞을 경우 Lean으로 번역할 확률이 높음. 즉, 영어 증명이 탄탄하다는 강력한 신호가 됨
    일단 Lean으로 형식화되면, 그 증명이 올바르다는 데 의심의 여지가 없음. 이것이 우리의 핵심 접근법임 — AI 기반 탐색을 통해 답을 찾으면, 그 복잡성에 상관없이 결과의 정확성을 보장받을 수 있음

    • AI가 Lean으로 번역한 증명이 정말로 문제의 올바른 형식화인지 어떻게 검증하는지 궁금함. 다른 분야에서 생성형 AI는 그럴듯한 거짓말을 잘 만들어내기 때문에, 이 경우에도 그럴 가능성이 있는지 알고 싶음
    • 이런 기술을 소프트웨어 검증에 적용하려는 시도가 있는지 궁금함
      Rust는 메모리 안전성을 보장하기 위해 고정된 규칙 집합을 사용하지만, 이 규칙이 단순하고 제한적임. 만약 Aristotle 같은 시스템이 컴파일러에 통합되어, 코드의 정확성 증명이 가능하면 자동으로 통과하도록 할 수 있다면 정말 멋질 것 같음
    • 새로운 LLM을 쓸 때마다 진짜 진보인지 단순한 벤치마크 해킹인지 헷갈리는데, 수학 증명의 형식화는 진짜 발전을 보여주는 지표라고 생각함
      Harmonic이 인간이 쓴 대부분의 수학을 형식화할 수 있으려면 얼마나 걸릴지 궁금함. 경쟁자인 Christian Szegedy는 올해 안에 가능하다고 하던데
    • 영어 증명이 맞을 경우 Lean으로 번역될 확률이 높다고 했는데, 이게 수학의 분야별 난이도에 따라 달라지는지 궁금함. 아직도 많은 연구 분야는 인간조차 형식화하기 어렵다고 알고 있음
    • “명제가 올바르게 형식화되었다면”이라는 전제가 꽤 큰 가정처럼 들림. 최근 Navier-Stokes 사건에서도 보았듯, 형식화 자체가 쉽지 않음

  • Terence Tao의 설명을 보면, 인간이 두 개의 AI 도구 사이에서 결과를 주고받으며, AI가 인간이 찾은 빈틈을 메우는 역할을 한 것으로 보임
    완전한 자율적 해결이라기보다는 인간과 AI의 협업에 가까움. 즉, 전문가가 주도하고 AI가 보조하는 형태임

    • 맞음, 실제로 Aristotle과 ChatGPT, 그리고 매우 뛰어난 사용자가 상호작용하며 진행한 것으로 이해함
    • 나는 Tao나 커뮤니티가 직접 빈틈을 찾은 게 아니라, 자동 증명 검증기를 사용했다고 들었음. 오히려 AI 90% / 인간 10% 정도의 비율로 보임
    • Reddit에 작성자의 자세한 설명이 있음 — reddit 게시물
    • 인간의 전문성과 노력 수준을 이해하려면 Erdős 문제 포럼의 스레드를 읽어보길 권함
    • 참고로, 이 사이트는 수학자 Thomas Bloom이 만들었고, ChatGPT가 기술적 설정을 도와줌 (FAQ 인용)

  • 기존 증명을 재구성하거나 새로운 방식으로 조합하는 작업이 인간에게는 지루하거나 복잡한 과정이지만, AI는 이를 초인적인 속도로 수행할 수 있음
    이런 접근은 AGI 이전 단계에서도 엄청난 가능성을 열어줄 것임. 수학자들이 AI를 도구로 활용해 밀레니엄 문제 같은 난제를 다루는 시대가 올 것 같음

    • 기존 증명을 재구성하는 것과 완전히 새로운 수학을 만드는 것 사이에는 명확한 경계가 없다고 생각함
    • 수학이 논리적이기 때문에 이미 이런 탐색을 위한 알고리즘이 많을 텐데, 단순한 탐색 문제로 보이지 않음
    • 나도 기존 증명 재구성 부분에는 동의함. LLM이 내놓은 결과를 검증하는 건 여전히 지루한 작업이지만, 인간이 직접 하는 것보단 낫다고 봄
      LLM의 진짜 가치는 언어로 표현 가능한 주제에서 새로운 관점을 제시하는 데 있음
    • 나는 이런 현상을 “과학적 리팩토링”이라 부름. 예를 들어, 어떤 상수를 바꿔서 논리를 다시 전개해보는 식의 실험을 AI가 자동으로 수행할 수 있게 됨
    • 복잡한 정리를 증명할 수 있는 AI가 AGI가 아니라면, 과연 무엇이 AGI인지 의문임

  • 실제 문제를 푼 사람이 작성한 설명글을 보면, 거대한 파이프라인 없이 단 몇 개의 프롬프트만으로 결과를 얻었다는 점이 인상적임
    최근 모델들은 훨씬 더 많은 연산 자원을 쓰는데, 이건 오히려 하한선 수준의 성과로 보임

  • Terence Tao가 “AI contributions to Erdős problems”라는 위키 페이지를 만들었음
    GitHub 페이지와 Mathstodon 글을 보면, 이번 결과(문제 728)는 그 페이지의 첫 번째 ‘초록색 항목’ , 즉 AI가 실제로 해결한 첫 사례임

    • 흥미롭게도, 위키의 6번 섹션에 있는 대부분의 AI 형식화 증명은 최근 몇 달 사이에 완성된 것임. 앞으로가 기대됨

  • 물리학이나 수학처럼 복잡한 분야의 전문가들도 AI와 대화하며 도움을 받는지 궁금함

    • 나는 순수수학 박사 후 데이터 과학자로 일하고 있음. 문헌 검토나 익숙하지 않은 수학을 빠르게 복습할 때 AI가 큰 도움이 됨
      분야별로 보면, 프로그래밍 > 응용 ML > 통계/응용수학 > 순수수학 순으로 유용성이 줄어듦
    • 나는 물리학 전공은 아니지만, AI 덕분에 필요한 공식이나 논문을 찾는 시간이 크게 줄었음. 다만 결과를 항상 검증해야 함
    • 딥러닝 모델과 새로운 attention 구조를 연구하는 입장에서, ChatGPT는 논문 검색과 연관 아이디어 탐색에 매우 유용함
    • 수학을 취미로 하는 입장에서, LLM은 내 시도에 피드백을 주거나 기존 해법으로 안내해줌. 놀이로서의 수학에는 꽤 즐거운 도구임
    • 대수기하 연구를 하는데, 문헌 검색 외에는 아직 큰 도움은 못 받음. 모델마다 편차가 큼

  • 지금 바로 Aristotle을 직접 써볼 수 있음 — https://aristotle.harmonic.fun/

    • AI를 DeepMind의 formal-conjectures 데이터셋으로 테스트해보는지도 궁금함
    • 문서에 “uvx aristotlelib@latest aristotle”이라고 되어 있는데 실제로는 “uvx --from aristotlelib@latest aristotle”이 맞음
      또, Stanford 개인 페이지 링크가 잘못되어 있음 (www 제거 필요)
    • 이건 별도의 HN 스레드로 다뤄야 할 만큼 흥미로움. CEO라면 직접 소개 글을 올려보는 것도 좋을 듯 (참고 링크)

  • 이번 결과는 정수에 대한 정리로, Mathlib 인프라가 잘 지원하는 영역임
    사용된 정의도 복잡하지 않아, 이런 유형의 증명은 성공 확률이 높음. 그래도 정말 놀라운 성취임

  • LLM을 넘어선 전문화된 AI 접근법의 가능성을 보여주는 사례임
    Aristotle 논문은 arXiv:2510.01346에 있음
    Transformer 구조를 썼다고 해서 모두 LLM은 아님 — 언어 데이터로 학습하지 않으면 LLM이라 부를 수 없음

    • 많은 사람들이 “LLM”을 “GenAI”와 혼용해서 쓰기 때문에 혼란이 생기는 듯함
    • “LLM이 아닌 접근법”이라 했는데, 실제로는 ChatGPT가 사용된 것 아님?
    • 맞음, 실제로는 ChatGPT가 사용되었음
    • 논문을 보면, 세 단계 모두 대형 트랜스포머 기반 LLM이 관여함
      1. Monte Carlo Graph Search에서 정책/가치 함수를 담당
      2. 비공식 추론 시스템이 chain of thought를 사용
      3. AlphaGeometry 역시 신경-기호적 언어 모델을 사용함
        즉, 모든 단계가 LLM 기반임

  • 2026년에는 AI가 수학의 미해결 문제를 점점 더 많이 다루게 될 것 같음
    이번 사례도 완전 자율은 아니지만, 인간의 피드백 후 AI가 거의 스스로 해결한 수준임
    이제 “LLM은 단순한 확률적 앵무새”라는 논쟁은 끝났다고 봄. 앞으로는 어떻게 실용화할지가 진짜 논의의 중심이 될 것임

    • 2026년에는 수학 분야에서 폭발적인 진전이 있을 것 같음
    • 이번 결과는 훈련 데이터에 있던 유사 증명의 리믹스일 가능성이 높지만, 그 리믹스 능력 자체가 강력함
    • 여전히 독립적인 검증이 필요함. 기업의 주장만으로는 신뢰하기 어려움
답변달기