← 블로그

해설21분 분량

AI는 에르되시 문제를 몇 개나 풀었을까: 2026년 10월 기준 집계와 그 한계

AI가 푼 에르되시 문제를 지금 세는 곳은 없습니다. 6월에 멈춘 위키, 해결 표시를 없앤 erdosproblems.com, AlphaProof Nexus와 OpenAI 결과를 날짜별로 정리했습니다.

목차
  1. 에르되시 문제는 몇 개이고, 몇 개나 풀렸나요?
  2. AI는 에르되시 문제를 몇 개나 풀었나요?
  3. AlphaProof Nexus는 무엇을 풀었나요?
  4. AI가 에르되시의 단위 거리 문제를 풀었나요?
  5. 대부분은 문헌 검색이었나요?
  6. 그 밖에 AI가 풀었다는 에르되시 문제는?
  7. 집계는 왜 멈췄나요?
  8. 증명에 대한 AI의 도움은 어떻게 표기해야 하나요?
  9. 다음 'AI가 에르되시 문제를 풀었다' 기사를 읽는 법
  10. Papex는 어디에 있나요?
  11. 출처

지금 AI가 푼 에르되시 문제의 수를 꾸준히 세는 곳은 없습니다. 집계를 하던 두 공개 기록이 모두 멈췄기 때문입니다. 테런스 타오가 시작한 위키 「AI contributions to Erdős problems」는 2026년 6월 30일 자료를 마지막으로 갱신을 멈췄습니다. 그때까지 AI가 주된 역할을 하고 결과가 '완전한 해결'로 표시된 항목이 하나 이상 있는 문제는 Papex가 표를 세어 본 바로 69개였습니다. 다만 위키는 이런 숫자를 점수처럼 읽지 말라고 경고합니다. 에르되시 문제 1,221개를 모은 Thomas Bloom의 erdosproblems.com은 2026년 10월 6일부터 문제별 해결 여부를 표시하지 않습니다. 마지막 집계는 해결 586개(48%)였는데, 사람과 AI의 기여를 구분하지 않은 숫자였습니다. 6월 이후 구글 딥마인드는 AlphaProof Nexus 연구를 Science에 발표했고(시도한 353개 중 해결 9개), OpenAI는 에르되시 문제 25개에 대한 주장을 담은 원고를 공개했습니다. Bloom은 이 원고들을 "주장으로 읽어야 한다"고 말합니다. 그리고 'AI가 에르되시 문제를 풀었다'는 첫 물결의 상당 부분은 문헌 검색이었습니다. 미해결로 표시된 문제에 이미 답한 논문을 AI가 찾아낸 것입니다.

이 글은 숫자와 그 출처, AlphaProof Nexus와 OpenAI의 단위 거리 결과가 보여 주는 것, 문헌 검색이 차지한 비중, 그 밖의 주요 주장, 집계가 멈춘 이유, AI의 기여를 어떻게 표기하자는 논의가 있는지, 그리고 다음 기사를 읽을 때 던질 여섯 가지 질문을 정리합니다. 모든 페이지는 2026년 10월 21일에 확인했습니다. 이 글의 숫자는 모두 '그날 기준'이며, Papex가 직접 센 숫자는 어떻게 셌는지 함께 적었습니다.

에르되시 문제는 몇 개이고, 몇 개나 풀렸나요?#

erdosproblems.com에는 1,221개가 올라 있습니다. 마지막으로 공개된 숫자는 2026년 10월 5일의 해결 586개(48%)이며, 10월 6일부터는 해결 여부를 전혀 표시하지 않습니다.

이 사이트는 에르되시 팔(Paul Erdős)이 남긴 문제를 모은 대표적인 온라인 목록으로, 맨체스터 대학교의 Thomas Bloom이 운영합니다. 10월까지는 첫 화면에 누적 숫자가 있었고, 인터넷 아카이브 사본으로 변화를 볼 수 있습니다.

보관된 첫 화면문제 수해결
2025년 10월 10일1,080397 (37%)
2026년 1월 2일1,133451 (40%)
2026년 7월 1일1,217553 (45%)
2026년 8월 5일1,217565 (46%)
2026년 10월 5일1,221586 (48%)

여기서 '해결'은 사이트가 문제의 상태를 증명됨, 반증됨, 기타 해결로 바꿨다는 뜻이며, 실제 해결보다 한참 뒤에 바뀐 경우도 있습니다. 사이트의 상태 변경 목록도 그것은 "이 사이트에서 상태가 바뀐 시점일 뿐 그 이상의 의미는 없다"고 적었습니다. 이전 속도를 가늠하자면, Quanta Magazine은 2024년부터 2025년 첫 8개월 사이에 111개 문제의 상태가 '미해결'에서 '해결'로 바뀌었다고 전합니다.

GitHub의 공동체 데이터베이스 teorth/erdosproblems는 지금도 합계를 공개합니다. 2026년 10월 20일 기준으로 증명 336개, 반증 139개, 기타 방식으로 해결 101개, 그리고 "완전히 열려 있는 것으로 보이는" 593개를 집계했고, 나머지는 더 작은 분류에 들어갑니다(2026년 10월 31일에 다시 확인한 숫자도 같습니다). 이 저장소는 자신의 상태 분류를 "비공식 크라우드소싱 분류"라고 부르며, 10월 6일부터는 방문자가 해결 문제 수를 처음부터 보지 않도록 합계를 첫 화면에서 뺐습니다. 두 출처의 숫자가 왜 다른지는 어느 쪽도 설명하지 않습니다.

AI는 에르되시 문제를 몇 개나 풀었나요?#

현재 숫자는 없습니다. 가장 자세한 기록인 위키 「AI contributions to Erdős problems」는 "이 위키는 더 이상 갱신되지 않는다. 최신 자료는 2026년 6월 30일 기준이다"라는 문장으로 시작합니다.

타오가 2025년 12월 27일 이 페이지를 만들었고, 멈출 때까지 1,096번의 편집 대부분은 Nat Sothanaphan이 했습니다. 위키는 AI의 기여를 AI가 맡은 역할과 이미 문헌에 있던 내용에 따라 나눴습니다. 아래 정의는 위키의 것이고, 숫자는 Papex가 센 것입니다.

위키 항목뜻완전한 해결이 있는 문제 수
1(a) AI 단독AI가 주된 역할, 비교할 만한 기존 문헌 없음, 사람의 개입은 "크지 않음"18
1(b) AI와 기존 문헌1(a)와 같지만 비교할 만한 문헌을 "나중에" 발견14
1(c) 문헌 위에 쌓은 AI1(a)와 같지만 비교할 만한 문헌을 "미리" 알고 있었음5
1(d) 사람과 협업한 AIAI가 주된 역할, 사람의 개입이 "큼"35
2(a) 문헌 검색AI로 문헌을 검색해 문제를 이미 해결한 기존 연구를 찾음31

센 방법은 이렇습니다. 멈춘 페이지에서 결과 칸이 위키의 초록색 표시와 "Full solution"(2(a)에서는 "Full solution found")으로 시작하는 행의 서로 다른 문제 번호를 셌습니다. 한 문제가 여러 항목에 들어갈 수 있어서 앞의 네 줄을 더하면 72개 항목, 69개 문제가 됩니다. 페이지에는 부분 결과, 검증되지 않은 주장, 잘못된 결과도 기록되어 있고, 1(a) 항목에만 '잘못됨'으로 표시된 행이 10개 있습니다.

위키는 이 표가 부추기는 읽기를 하지 말라고 합니다. 첫 번째 주의 사항이 "이 페이지는 벤치마크가 아니다"이고, 서로 다른 방법으로 푼 문제의 숫자를 직접 비교하는 것은 사과와 오렌지를 비교하는 셈일 수 있다고 덧붙입니다. 타오도 1월에 AI 기여의 평가는 매우 복잡하고 미묘해서 단순한 순위표나 숫자로 줄일 수 없다는 요약을 더했습니다.

위키가 멈춘 뒤 AI 기여를 이렇게 나눠 기록하는 곳은 찾지 못했습니다. 10월에 Plasma AI라는 회사가 연 erdosproblems.ai는 문제마다 미해결, 주장됨, 해결 상태를 붙이고(10월 21일 기준 미해결 494, 주장됨 110, 해결 617), 증명을 제출할 때 기여자와 사용한 도구를 적게 합니다. 이 사이트는 독립적으로 운영되며 Bloom의 지지를 뜻하지 않는다고 밝히고, AI 결과의 수는 따로 집계하지 않습니다.

AlphaProof Nexus는 무엇을 풀었나요?#

시도한 353개 가운데 9개 항목을 풀었고, 모두 Lean 증명이 있습니다. 구글 딥마인드, 구글, 오르후스 대학교의 George Tsoukalas 외 20명이 쓴 논문 「Advancing mathematics research with AI-driven formal proof search」가 5월 프리프린트에 이어 2026년 10월 8일 Science에 실렸습니다. 초록은 353개의 미해결 에르되시 문제 가운데 9개를 자율적으로 해결한 형식 증명 탐색 에이전트를 만들었다고 말합니다.

353개는 어떻게 골랐나. 사람이 고르지 않았습니다. 연구진은 2026년 2월 초 Formal Conjectures 저장소에 있던 에르되시 문제의 Lean 명제 전부, 즉 353개에 에이전트를 돌렸고, 이 방식에는 Lean으로 형식화하기 쉬운 문제 쪽으로 치우치는 편향이 있다고 적었습니다.

'해결'의 뜻. 에이전트는 형식 명제에 대해 빈틈 없는 완전한 Lean 증명을 만들어야 했습니다. 그다음 연구진의 전문가가 Lean 명제가 원래 추측을 충실히 담았는지 확인했습니다. 두 문제는 명제 자체가 바뀌었습니다. 에이전트가 '밀도'라는 말을 다른 뜻으로 써서 증명을 찾은 뒤, 그 말을 '하밀도(lower density)'와 '상밀도(upper density)'로 고쳤습니다. 일반 수학 언어로 된 증명은 사람이 썼습니다. 논문의 기여 설명에 따르면 연구진 여섯 명이 자연어 증명을 썼고, 한 명이 에이전트가 만든 초안을 제공했습니다.

아홉 항목. 논문의 표 1은 erdosproblems.com 번호로 아홉 항목을 적습니다. 일부는 문제의 한 부분이거나 변형입니다.

항목논문이나 사이트가 덧붙인 내용
#12 (i), (ii)해법이 공유된 뒤 원래 논문의 구성을 조금 고쳐 같은 질문에 답할 수 있었음. 세 번째 부분은 아직 열려 있음
#26†에르되시가 낸 질문의 더 일반적인 변형이며, 에르되시 자신이 낸 문제는 아님
#125명제를 '하밀도'로 수정
#138*문제의 변형
#152Bloom은 처음에 기존 방법으로 풀린다고 생각했다가 5월 16일 "완전히 틀렸다"고 적음
#741 (i), (ii)(i)은 '상밀도'로 수정. 사이트에 따르면 (ii)는 OpenAI 모델이 독립적으로 답함
#846OpenAI 내부 모델도 독립적으로 발견했으며, 사이트는 Reiher, Rödl, Sales(2024)의 사영 논증에서도 따라 나온다고 적음

단순한 에이전트도 풀었다. 프리프린트는 기본 에이전트도 어려운 문제에서는 비용이 더 들었지만 9개를 모두 풀었다고 적었고, Science 초록에도 이 내용이 남아 있습니다. 6월판 프리프린트는 두 코딩 에이전트도 시험했습니다. Codex는 12시간 안에 #152와 #125를 풀지 못해 9개 중 7개를 풀었고, Claude Code로는 한 문제도 풀지 못했다고 적었습니다. Papex는 6월 8일 arXiv판을 읽었고 Science 전문은 보지 못했습니다. Science 초록에는 프리프린트에 있던 '문제당 수백 달러'라는 비용 문구가 더 이상 없습니다. 프리프린트는 풀 만한 문제를 찾는 일 자체에 상당한 계산 자원이 들었다고도 덧붙였습니다.

Bloom은 Science News에 이 결과들이 중요도로 보면 최상위 수준은 아니라고 말하면서, 구글 딥마인드가 과학적으로 더 책임 있게 하려고 노력했다고 평가했습니다. 같은 호 Science에는 Jeremy Avigad와 Matthew Ballard의 관점 글 「AI for research mathematics has arrived」가 실렸습니다.

AI가 에르되시의 단위 거리 문제를 풀었나요?#

에르되시의 추측을 반증했고, OpenAI 밖의 수학자들이 그 증명을 확인하고 다듬었습니다. erdosproblems.com의 #90 문제입니다.

에르되시는 평면 위 n개의 점 가운데 거리가 정확히 1인 쌍이 최대 몇 개일 수 있는지 묻고, 1946년에 그 수가 n보다 아주 조금 빠르게만 늘어난다고 추측했습니다. 2026년 5월 20일 OpenAI는 내부 모델이 이 오래된 추측을 반증했으며 다항식 크기의 개선을 주는 무한한 예를 찾았다고 발표했습니다. 이 구성은 무한히 많은 n에 대해, 고정된 δ > 0으로 단위 거리 쌍이 적어도 n^(1+δ)개인 n개의 점을 줍니다. 같은 날 프린스턴의 Will Sawin은 n^1.014보다 많게 만들 수 있음을 보였습니다. OpenAI는 증명이 '새로운 범용 추론 모델'에서 나왔다고만 하고 모델 이름은 밝히지 않았습니다.

같은 날 Noga Alon, Bloom, 팀 가워스(Tim Gowers) 등 수학자 아홉 명이 동반 논문을 올렸습니다. 사람이 검증하고 소화한 짧은 판본으로, 논증이 적어도 돌이켜 보면 Ellenberg-Venkatesh, Golod-Shafarevich, Hajir-Maire-Ramakrishna의 아이디어에 결정적으로 기댄다고 적었습니다. 아홉 명 중 한 명인 Melanie Matchett Wood는 Scientific American에 문헌에 출처가 밝혀지지 않은 매우 비슷한 아이디어가 있었으며, 사람이 그 결과를 알면서도 밝히지 않았다면 직업적 과실이었을 것이라고 말했습니다. 가워스는 OpenAI 페이지에 실린 의견에서, 사람이 Annals of Mathematics에 냈다면 주저 없이 게재를 추천했을 것이라고 썼습니다.

엿새 뒤 Anthropic에서 일하는 Levent Alpöge는 'mythos'가 이 문제를 풀 수 있는지 확인했고 답은 '그렇다'였다고 X에 올렸고, Anthropic 사이트에 저자나 모델을 밝히지 않은 해설을 올렸습니다. erdosproblems.com 토론방의 한 참여자는 이 해설이 추측의 약한 형태만 다룬다고 지적했고, Bloom은 매개변수를 더 잘 고르면 강한 결과도 나올 것이라고 답하면서 정확성을 보증하는 것은 아니라고 덧붙였습니다.

이 문제의 페이지는 사이트의 새 방식을 보여 줍니다. 5월에는 "OpenAI의 내부 모델이 반증했다"고 적혀 있었지만, 10월 중순부터는 "반증되었다"는 문장 뒤에 결과와 논문 링크만 붙어 있습니다.

대부분은 문헌 검색이었나요?#

처음에는 그랬습니다. 2025년 10월 erdosproblems.com의 기여자 몇 명이 미해결로 표시된 문제의 문헌을 AI 연구 도구로 찾기 시작했습니다. 2025년 10월 16일 타오는 이 방식으로 '미해결'에서 '해결'로 바뀐 문제를 여섯 개로 셌습니다.

다음 날 당시 OpenAI에 있던 Kevin Weil은 GPT-5가 수십 년 동안 풀리지 않은 에르되시 문제 10개의 해법을 찾고 11개에서 진전을 이뤘다고 올렸습니다. Bloom은 "극적인 왜곡"이라며, GPT-5는 자신이 몰랐던 기존 해법 논문을 찾았을 뿐이고 사이트의 '미해결'은 자신이 그 문제를 푼 논문을 모른다는 뜻일 뿐이라고 답했습니다. Weil은 글을 지웠고, 구글 딥마인드의 데미스 허사비스는 OpenAI 연구원의 비슷한 글에 "민망한 일"이라고 답했습니다.

Bloom은 2026년 1월 이렇게 정리했습니다. 처음에는 '강력한 문헌 검색'으로 몰랐던 해법과 논문이 많이 나왔고, 지난 한 달 사이 AI가 만든 실제 해법이 보이기 시작했다는 것입니다. 타오는 두 경우가 섞이는 이유를, AI가 먼저 풀 수 있는 문제가 바로 문헌에서 이미 풀렸을 가능성이 가장 큰 '명목상 미해결' 문제이기 때문이라고 설명했습니다. 2025년 크리스마스에는 AI가 자율적으로 풀었다던 #333 문제가 몇 시간 만에 에르되시 자신의 1977년 논문에 이미 있는 것으로 밝혀졌습니다. 구글 딥마인드는 2026년 1월 사례 연구에서 미해결로 표시된 13개 문제를 다뤘는데, 5개는 새로운 것으로 보이는 자율적 해법으로, 8개는 기존 문헌의 해법을 찾아내는 방식으로 해결됐다고 보고하며, 이 문제들이 '미해결'이었던 이유는 어려움보다 잘 알려지지 않았기 때문이라고 결론지었습니다.

그 밖에 AI가 풀었다는 에르되시 문제는?#

2026년에 알려진 주요 주장을 출처가 밝힌 대로 정리하면 다음과 같습니다.

문제시기주장출처가 덧붙인 내용
#728, 계승의 나누어떨어짐1월Kevin Barreto가 GPT-5.2 Pro와 Harmonic의 Aristotle로, Lean 증명해설 논문은 AI가 자율적으로 완전히 해결한 첫 에르되시 문제로 봄. 사이트는 문제 원문이 '모호'하고 의도한 취지에 대한 답이라고 표시
#1196, 원시 집합4월Liam Price가 프롬프트를 준 GPT-5.4 ProJared Duker Lichtman은 Scientific American에 ChatGPT의 원래 증명은 꽤 부실했다고 말함. 이후 8인 공저 논문
#146, #180, #1838월 1일OpenAI의 'Astra 내부 버전', Lean 인증서OpenAI: 정확성은 자사가 책임지며 수학적 논증 자체는 시스템이 생성
25개 문제10월 6일OpenAI openai/math 공개분(현재 원고 719편)Bloom: 모두 '주장'으로 읽어야 하며, 25개 중 21개 증명이 Lean으로 형식화됨
#508, 하드비거-넬슨 문제10월 6일같은 공개분. 평면을 다섯 색으로 칠하면 반드시 거리 1인 같은 색 두 점이 생긴다는 주장사이트는 현재 6 ≤ χ ≤ 7로 표시하고 형식 증명을 링크

10월 공개분에 대해 Bloom의 개관은 논문들이 언뜻 보기에 AI 특유의 방식으로 매우 형편없이 쓰였다고 평하면서, 대부분은 맞지만 전문가가 보면 크게 단순화하고 개선할 수 있을 것으로 예상했습니다. 저장소 설명 파일도 형식화되지 않은 결과 가운데 일부는 문제가 있을 수 있다고 적었습니다. OpenAI는 10월 7일 에르되시 문제와 무관한 원고 세 편을 철회하고 14편을 수정했습니다. 철회된 세 편은 호지 추측에 관한 원고로, 밀레니엄 문제 글에서 다뤘습니다.

집계는 왜 멈췄나요?#

숫자 자체가 목표가 되었기 때문입니다. Bloom은 2026년 10월 6일 네 가지 변경을 발표했습니다. 새 문제 댓글과 증명 주장의 접수 중단, 해결 여부 표시 중단, 사람이든 AI든 결과에 공로를 부여하는 표현 중단, 그리고 해설 강화입니다. 그는 사람들이 이 사이트를 주로 AI가 만든 증명을 설명 없이 광고하고 점점 의미가 없어지는 우선권 주장을 남기는 데 쓰게 됐다고 이유를 밝혔습니다.

해결 여부를 없앤 것은 그저 문제를 AI에 넣고 '미해결에서 해결로' 바뀌는 쾌감을 좇는 사람들을 줄이고, '해결된 문제의 비율'에서 잘못된 결론을 끌어내지 않게 하려는 것이라고 했습니다. 결과는 계속 기록하되 'Bloom이 x > y를 증명했다' 대신 'x > y가 알려져 있으며 증명 해설은 Bloom이 제공한다'처럼 쓰겠다고 했습니다. AI 증명을 모으는 저장소에 대해서는 자신이 맡고 싶지 않으며, 그런 저장소와 질문 자체를 알리려는 사이트는 분리되어야 한다고 적었습니다.

위키는 멈춘 이유를 밝히지 않았습니다. 주 관리자인 Sothanaphan은 7월에 위키의 형식이 무엇을 기여로 칠지를 은연중에 제한했다고 썼습니다. 증명 생성이 증명 검증과 증명 소화보다 우선시됐는데, 자신은 그 둘도 못지않게 중요하다고 본다는 것입니다.

이제 돈은 확인 작업으로 가고 있습니다. 10월 15일 사이먼스 재단은 Anthropic, OpenAI와 함께 1,500만 달러 규모의 자금과 자원을 투입해 연구자들이 최근 AI 지원 결과를 평가하고, 새 도구를 배우고, AI 사용에 관한 공동 기준을 만드는 일을 돕겠다고 발표했습니다. OpenAI와 Anthropic은 각각 500만 달러를 낸다고 밝혔습니다. 관련 공모 「Targeted Grants to Math+AI Institutes」는 2026년 12월 1일에 마감합니다.

증명에 대한 AI의 도움은 어떻게 표기해야 하나요?#

수학계는 아직 정하는 중이지만, 글로 정해진 원칙도 몇 가지 있습니다.

  • 도구는 밝히고 공로는 사람에게. 2026년 6월의 라이덴 선언(Leiden Declaration)은 대규모 언어 모델을 포함한 자동화 도구의 사용을 투명하게 밝히라고 하고, 공로와 책임은 계속 수학 공동체의 사람에게 속하며 자동화 시스템에 주어져서는 안 된다고 말합니다. 선언 사이트는 국제수학연맹의 지지를 받았다고 밝힙니다.
  • AI 사용을 밝히지 않으면 소개하지 않는다. Bloom은 10월 글에서 논문이 출처를 밝히고 AI를 어떻게 썼는지 정직하게 공개해야 하며, 표절이나 AI 사용에 관한 허위의 증거가 있으면 증명이 맞더라도 소개하지 않을 수 있다고 적었습니다.
  • Lean 증명을 어떻게 만들었는지 밝힌다. Lean으로 검증된 결과를 모으는 Palomar 등록부는 항목마다 formalization.yaml 파일을 요구하고, 필수 항목인 자동화 수준에 "manual | copilot | agent | autonomous | other" 중 하나를 적게 합니다.
  • 만든 시스템에 결과를 돌린다. OpenAI는 자사 결과에 이 방식을 씁니다. AI 시스템이 전적으로 생성한 증명에 사람을 저자로 내세우면 시스템의 기여와 사람의 진짜 지적 작업을 모두 잘못 나타내게 된다는 이유입니다.

타오는 우선권 자체에 대해 더 나아간 제안을 했습니다. 8월 6일, 프리프린트나 형식 증명 인증서를 먼저 낸 사람에게 우선권을 주면 누가 AI에 가장 빨리 프롬프트를 넣느냐의 경쟁이 되므로, 결과를 처음으로 명확하게 제시한 저자에게 주자고 제안했습니다. 후속 글에서는 증명을 생성 산출물(AI 대화 기록 등), 검증 산출물(Lean 코드 등), 해설 산출물(녹화된 강연 등), 출판 산출물로 나누고, 연구자가 각 단계의 부분 진전을 이룬 날짜를 타임스탬프로 남긴 비공개 저장소를 두었다가 준비되면 공개하는 모습을 그렸습니다. 진행 중인 연구를 암호화된 해시로 알리는 방안도 언급했지만, 그것이 바람직한 방향인지는 확신하지 못한다고 덧붙였습니다.

다음 'AI가 에르되시 문제를 풀었다' 기사를 읽는 법#

위 사례에서 뽑은 여섯 가지 질문입니다. 더 큰 문제에 대한 주장은 AI는 밀레니엄 문제를 풀었을까를 참고하십시오.

  1. 몇 번 문제의 어느 부분인가? 많은 문제에 부분과 변형이 있습니다. AlphaProof Nexus의 9개에는 #12의 두 부분, #741의 두 부분, 그리고 에르되시 자신이 낸 것이 아닌 #26의 변형이 들어 있습니다.
  2. 이미 알려진 결과가 아닌가? 문제 페이지와 참고문헌을 확인하십시오. 문헌 검색으로 많은 '미해결' 문제의 답이 나왔고, #333은 에르되시 자신의 1977년 논문에 있었습니다.
  3. Lean 명제는 누가 썼나? Lean 증명은 그것이 증명하는 명제만큼만 의미가 있습니다. 위키의 조언은 결과의 명제를 증명하는 AI가 아니라 사람이나 제3자가 형식화하는 것이 가장 좋다는 것입니다.
  4. 사람이 따라갈 수 있는 증명이 있나? Bloom은 Palomar에서 검증된 올바른 Lean 형식화는 링크하려 하지만, 설명이 부실하고 형식화도 없는 증명으로 사이트를 갱신할 가능성은 낮다고 말합니다.
  5. 사람은 무엇을 했나? 문제 선택, 프롬프트 작성, 명제 수정, 증명 정리가 모두 기여입니다. AlphaProof Nexus에서도 연구진이 에이전트의 초안을 참고해 자연어 증명을 썼습니다.
  6. 연구실 밖의 누가 확인했나? 이름을 밝힌 수학자 아홉 명이 공동 논문으로 소화한 단위 거리 결과와, Bloom이 '주장'으로 분류한 10월 공개분을 비교해 보십시오.

Papex는 어디에 있나요?#

Papex는 에르되시 문제를 세지 않고, 증명을 검토하지 않으며, Lean을 실행하지 않습니다.

Papex의 미해결 문제 목록에는 에르되시가 낸 문제도 일부 있습니다. 에르되시-스트라우스 추측(erdosproblems.com #242), 에르되시와 라도의 해바라기 추측(#20), 하드비거-넬슨 문제(#508)입니다. 하드비거-넬슨 페이지의 'AI-assisted claims' 항목은 OpenAI의 다섯 색 주장을 출처가 밝힌 그대로, Bill Gasarch가 공개한 반응과 함께 보여 줍니다. 항목에는 "Claims as their sources state them. Papex has not checked them; the status stays the source’s."라는 안내가 붙습니다. 출처가 밝힌 주장을 옮겼을 뿐 Papex가 확인하지 않았으며 상태는 출처의 판단을 따른다는 뜻입니다(화면은 영어입니다).

연구자에게 Papex는 연구 과정의 기록이며, 타오의 글에 나오는 그림과 닮은 부분이 있습니다. Papex에 연결된 AI 앱(AI 앱 연결 안내)은 비공개 초안을 준비하고, 작업 세션을 짧게 요약한 비공개 체크포인트를 남길 수 있습니다. 이 체크포인트는 소유자만 봅니다. 정확한 버전에 서명하는 것은 앱이 아니라 사람이며, 사용한 AI 도구는 그 사람의 이름 옆에 밝힙니다. AI 앱은 저자로 표시되지 않습니다. 서명한 버전은 OpenTimestamps로 타임스탬프를 받아 비트코인에 고정되며(지갑은 필요 없습니다), 이후 수정은 새 버전이 되므로 이력이 그대로 남습니다. 공개 기록은 문제와 연결되어 해당 페이지에 표시됩니다.

Papex 기록은 우선권 판정이 아닙니다. 증명이 맞다거나 독창적이라거나 최초라는 것을 보여 주지 않으며, 동료 심사도 아닙니다. 기록이 보여 주는 것은 이름이 밝혀진 사람이 어떤 버전에 언제 서명했고, AI가 무엇을 했다고 그 사람이 밝혔는지입니다. 모델 이름은 그 사람이 밝힌 그대로입니다.

출처#

모두 2026년 10월 21일 확인

다른 글

모든 글