나는 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% 정도의 비율로 보임
참고로, 이 사이트는 수학자 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은 내 시도에 피드백을 주거나 기존 해법으로 안내해줌. 놀이로서의 수학에는 꽤 즐거운 도구임
문서에 “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이 관여함
Monte Carlo Graph Search에서 정책/가치 함수를 담당
비공식 추론 시스템이 chain of thought를 사용
AlphaGeometry 역시 신경-기호적 언어 모델을 사용함
즉, 모든 단계가 LLM 기반임
2026년에는 AI가 수학의 미해결 문제를 점점 더 많이 다루게 될 것 같음
이번 사례도 완전 자율은 아니지만, 인간의 피드백 후 AI가 거의 스스로 해결한 수준임
이제 “LLM은 단순한 확률적 앵무새”라는 논쟁은 끝났다고 봄. 앞으로는 어떻게 실용화할지가 진짜 논의의 중심이 될 것임
2026년에는 수학 분야에서 폭발적인 진전이 있을 것 같음
이번 결과는 훈련 데이터에 있던 유사 증명의 리믹스일 가능성이 높지만, 그 리믹스 능력 자체가 강력함
Hacker News 의견들
나는 Harmonic에서 일하고 있으며, 우리가 만든 Aristotle에 대해 몇 가지 오해를 바로잡고 싶음
Aristotle은 최신 AI 기법을 적극적으로 활용하며, 언어 모델링도 포함함
영어로 된 비공식 증명을 입력하면, 그 증명이 맞을 경우 Lean으로 번역할 확률이 높음. 즉, 영어 증명이 탄탄하다는 강력한 신호가 됨
일단 Lean으로 형식화되면, 그 증명이 올바르다는 데 의심의 여지가 없음. 이것이 우리의 핵심 접근법임 — AI 기반 탐색을 통해 답을 찾으면, 그 복잡성에 상관없이 결과의 정확성을 보장받을 수 있음
Rust는 메모리 안전성을 보장하기 위해 고정된 규칙 집합을 사용하지만, 이 규칙이 단순하고 제한적임. 만약 Aristotle 같은 시스템이 컴파일러에 통합되어, 코드의 정확성 증명이 가능하면 자동으로 통과하도록 할 수 있다면 정말 멋질 것 같음
Harmonic이 인간이 쓴 대부분의 수학을 형식화할 수 있으려면 얼마나 걸릴지 궁금함. 경쟁자인 Christian Szegedy는 올해 안에 가능하다고 하던데
Terence Tao의 설명을 보면, 인간이 두 개의 AI 도구 사이에서 결과를 주고받으며, AI가 인간이 찾은 빈틈을 메우는 역할을 한 것으로 보임
완전한 자율적 해결이라기보다는 인간과 AI의 협업에 가까움. 즉, 전문가가 주도하고 AI가 보조하는 형태임
기존 증명을 재구성하거나 새로운 방식으로 조합하는 작업이 인간에게는 지루하거나 복잡한 과정이지만, AI는 이를 초인적인 속도로 수행할 수 있음
이런 접근은 AGI 이전 단계에서도 엄청난 가능성을 열어줄 것임. 수학자들이 AI를 도구로 활용해 밀레니엄 문제 같은 난제를 다루는 시대가 올 것 같음
LLM의 진짜 가치는 언어로 표현 가능한 주제에서 새로운 관점을 제시하는 데 있음
실제 문제를 푼 사람이 작성한 설명글을 보면, 거대한 파이프라인 없이 단 몇 개의 프롬프트만으로 결과를 얻었다는 점이 인상적임
최근 모델들은 훨씬 더 많은 연산 자원을 쓰는데, 이건 오히려 하한선 수준의 성과로 보임
Terence Tao가 “AI contributions to Erdős problems”라는 위키 페이지를 만들었음
GitHub 페이지와 Mathstodon 글을 보면, 이번 결과(문제 728)는 그 페이지의 첫 번째 ‘초록색 항목’ , 즉 AI가 실제로 해결한 첫 사례임
물리학이나 수학처럼 복잡한 분야의 전문가들도 AI와 대화하며 도움을 받는지 궁금함
분야별로 보면, 프로그래밍 > 응용 ML > 통계/응용수학 > 순수수학 순으로 유용성이 줄어듦
지금 바로 Aristotle을 직접 써볼 수 있음 — https://aristotle.harmonic.fun/
또, Stanford 개인 페이지 링크가 잘못되어 있음 (www 제거 필요)
이번 결과는 정수에 대한 정리로, Mathlib 인프라가 잘 지원하는 영역임
사용된 정의도 복잡하지 않아, 이런 유형의 증명은 성공 확률이 높음. 그래도 정말 놀라운 성취임
LLM을 넘어선 전문화된 AI 접근법의 가능성을 보여주는 사례임
Aristotle 논문은 arXiv:2510.01346에 있음
Transformer 구조를 썼다고 해서 모두 LLM은 아님 — 언어 데이터로 학습하지 않으면 LLM이라 부를 수 없음
즉, 모든 단계가 LLM 기반임
2026년에는 AI가 수학의 미해결 문제를 점점 더 많이 다루게 될 것 같음
이번 사례도 완전 자율은 아니지만, 인간의 피드백 후 AI가 거의 스스로 해결한 수준임
이제 “LLM은 단순한 확률적 앵무새”라는 논쟁은 끝났다고 봄. 앞으로는 어떻게 실용화할지가 진짜 논의의 중심이 될 것임