80년 난제를 AI가 깼다. 실제로 증명된 것은?

이름 없는 OpenAI 모델이 에르되시 단위거리 추측을 반증했다. Sawin의 n^1.014는 80년 만의 첫 지수 개선이다.

80년 난제를 AI가 깼다. 실제로 증명된 것은?
Share

약 80년 동안 수학자들은 평면에서 서로 같은 거리에 놓인 점들을 얼마나 조밀하게 배치할 수 있는지에 대해 폴 에르되시의 직관이 맞다고 믿었다. 2026년 5월, 한 AI 추론 모델은 그가 틀렸음을 보였다. 하지만 왜 틀렸는지 이해하려면 그가 정확히 무엇을 주장했는지부터 알아야 한다.

에르되시의 단위거리 추측은 무엇이었나

단위거리 문제는 겉보기에는 아주 단순한 질문을 던진다. 유클리드 평면에 n개의 점이 있을 때, 서로 정확히 거리 1만큼 떨어진 점쌍은 최대 몇 개일 수 있을까? 그 최댓값을 ν(n)이라고 하자. 즉 임의의 n점 배치 전체에서, 단위거리만큼 떨어진 순서 없는 점쌍의 가능한 최대 개수다 . 에르되시는 1946년에 이 문제를 제기했고, 이후 이 문제는 이산기하학의 핵심 질문이 되었다 .

에르되시의 하한 구성은 격자형이었다. 점들을 √n × √n 정수 격자처럼 배치하면 ν(n)은 n1+o(1) 차수가 된다 . 그는 이 구성에서 나아가, 이에 대응하는 거의 선형인 상한을 추측했다. 어떤 배치도 본질적으로 이보다 의미 있게 더 잘할 수 없다는 주장이다.

  • 추측: ν(n) ≤ n1+O(1/log log n). 여기서 지수는 n이 커질수록 1에 가까워진다. 다시 말해 격자가 본질적으로 최적이라는 뜻이다 .
  • 정식 명제: Erdős Problems 데이터베이스에는 이것이 문제 #90으로 올라와 있다. 모든 n점 평면 집합은 단위거리 점쌍을 최대 n1+O(1/log log n)개만 가질까?

두 가지 경계가 그 간극을 규정했다. 알려진 최선의 일반 상한은 O(n4/3)으로, 지수는 약 1.333이다. 이는 1984년 스펜서, 세메레디, 트로터가 증명했으며 40년 동안 개선되지 않았다 . (단위거리 그래프가 K2,3-free라는 사실에서 초등적인 O(n3/2) 상한도 따라온다.) 반면 하한의 지수는 80년 동안 1+o(1)에 머물러 있었다 .

핵심 미해결 질문은 고정된 δ > 0이 존재해서 무한히 많은 n에 대해 ν(n) ≥ n1+δ가 성립하는지였다. 양의 고정 δ가 있다면, 어떤 상수 C에 대해서도 결국 C/log log n을 넘어서게 된다. 이는 에르되시가 제시한 거의 선형의 천장을 형식적으로 깨뜨리고, 격자가 최적이 아님을 증명한다 . 수십 년 동안 지배적인 직관은 그런 δ가 존재하지 않는다는 쪽이었다. 무너진 것은 바로 그 직관이었다.

무엇이 반박됐고, 무엇이 남았나

An 80-year conjecture fell to AI. What was actually proved?

정리는 정확하고 범위도 좁다. 어떤 절대상수 δ > 0이 존재해서, 무한히 많은 n에 대해 ν(n) ≥ n1+δ가 성립한다는 것이다 . 결정적인 단어는 고정된이다. 에르되시가 추측한 천장은 n1+O(1/log log n)이었다. 즉 1을 넘는 지수의 초과분이 n이 커질수록 0으로 줄어드는 형태다. 양의 고정 δ는 어떤 상수 C에 대해서도 결국 C/log log n을 넘기 때문에, 새 구성은 충분히 큰 모든 n에서 그 천장을 뚫고 거의 선형 추측을 정면으로 반박한다 . 격자는 최적이 아니다.

이 결과가 무엇이 아닌지도 그만큼 중요하다. AI가 “단위거리 문제를 풀었다”고 말하는 제목들은 주장을 과장한 것이다. 이 모델은 더 나은 점 배치를 제시해 추측된 상한을 반박했을 뿐, ν(n)을 결정한 것은 아니며 정확한 점근적 성장률은 여전히 미해결이다 . 이는 ν(n)의 새로운 바닥을 놓은 하한의 진전이지, 완전한 해결은 아니다.

간극의 다른 쪽은 그대로다. 1984년 스펜서, 세메레디, 트로터가 증명한 최선의 일반 상한 O(n4/3)은 여전히 유효하다 . 따라서 이번 돌파 이후 ν(n)은 대략 1.014라는 지수(소윈이 제시한 새로운 명시적 하한)와 1.333(SST 상한) 사이에 놓이게 되었다 . 이 남은 간극은 여전히 크고 미해결이다. 이번 결과는 답의 가능한 범위를 좁혔지만, 닫지는 않았다.

결과ν(n)에 대한 경계유형연도
에르되시 격자 구성n1+o(1)하한1946
OpenAI 모델(존재 증명)n1+δ, δ > 0 정량화 없음하한2026
소윈(명시적)n1.014114하한2026
스펜서–세메레디–트로터O(n4/3) ≈ n1.333상한1984

수학계는 이 결과의 의미를 전체 문제의 해결이 아니라 추측의 반박이라는 틀 안에서 신중하게 설명했다. 노가 알론은 이를 오래된 미해결 문제를 정리한 뛰어난 성과라고 불렀다 . 이는 ν(n)을 결정했다기보다 하나의 추측을 반박했다는 말에 맞는 표현이다. 이 이야기를 따라가는 빌더에게 핵심은 정확한 범위다. 고정 지수의 개선은 사라져 가는 항을 조금 깎는 것과 질적으로 다르며, 여기서 무너진 것은 깔끔한 닫힌형 답이 아니라 바로 그 질적 도약이었다.

대수적 수론이 만든 연결고리

이 추측을 무너뜨린 구성은 평평한 격자를 대수적 수론에서 가져온 장치로 바꾸며, 바로 이 도입이 기술적으로 놀라운 부분이다. √n × √n 격자 위에 점을 배열하는 대신, 이 모델은 근판별식이 유계인 완전 실수체의 무한 타워를 만든다. 이는 Golod–Shafarevich 유형의 class-field-tower 이론과 Hajir–Maire–Ramakrishna 계열 연구가 보장하는 성질이다 . 판별식이 유계로 유지되기 때문에 최종 점 집합은 점근적으로 격자를 이길 만큼 충분히 조밀해진다.

그다음 단계는 다음처럼 이어진다.

  • i를 첨가해 CM 체를 만든다. 각각의 완전 실수체 L을 K = L(i)라는 CM 체로 확장하고, 이 복소 구조는 이후 사영에 쓰인다 .
  • 완전히 분해되는 유리 소수를 사용한다. K에서 완전히 분해되는 소수들은 많은 노름 1 원소를 만들어낸다. 절댓값이 정확히 1인 대수적 단위들이며, 단위 거리의 원천이다 .
  • Minkowski 격자에 매장한다. 이 원소들은 체의 매장들로 만든 고차원 Minkowski 격자 안에 놓인다.
  • 원판들의 곱으로 된 창으로 잘라낸다. 원판들의 곱 필터가 유한하고 잘 제어된 격자점 부분족을 골라낸다.
  • 하나의 복소 좌표로 사영한다. 하나의 복소 좌표로 사영하면 고차원 집합이 평면 점 집합으로 압축된다. 그리고 그 안에는 거리가 정확히 1인 쌍이 많이 들어 있다 .

수학자들이 특히 인상적이라고 본 지점은 이 연결 자체였다. class field tower와 분해 소수를 이산기하의 계수 문제에 연결한 선례가 없었기 때문이다. Noga Alon과 동료들의 동반 arXiv 노트(arXiv:2605.20695, 2026년 5월 20일 제출)는 짧고 사람이 검증한 버전을 재구성하며, 돌이켜보면 그 재료를 Ellenberg–Venkatesh, Golod–Shafarevich, Hajir–Maire–Ramakrishna의 아이디어로 돌린다 . 각각은 잘 알려진 도구였지만, 기여는 그 도구들을 이전에는 향한 적 없던 incidence geometry에 연결한 데 있었다.

이처럼 분야를 가로지르는 범위가 바로 인간 연구자들이 오랫동안 이 길을 놓친 이유이기도 하다. 단위 거리 구성을 위해 class-field tower를 활용하려면 수론과 조합기하 전반을 넘나드는 폭이 필요했는데, 이는 뚜렷하거나 보상받는 방향이 아니었다. 특히 Jacob Tsimerman은 비슷한 노선을 탐색했다가 너무 시간이 많이 든다고 보고 포기한 것으로 전해진다. 부족했던 것은 어떤 통찰 하나가 아니라 실패한 시도들이 쌓이는 "grind"였다는 것이다 .

"오래된 미해결 문제를 해결한 뛰어난 성취입니다." — Noga Alon, 수학자이자 동반 노트 공동 저자 (source: Understanding AI).

구축하는 사람들에게는 headline보다 기법이 더 중요하다. 이 성과는 완전히 새로운 수학을 발명해서가 아니라, 인간이 좀처럼 함께 넘나들지 않는 하위 분야들 사이에서 기존 장치들을 재조합해 나온 것이다. 이런 모델들이 연구 워크플로로 들어올수록 추적할 가치가 있는 능력의 양상이다.

AI의 자율성과 수학자가 실제로 기여한 것

An 80-year conjecture fell to AI. What was actually proved?

OpenAI 원고에서 가장 논쟁적인 주장은 수학적 내용이 아니라 절차에 관한 것이다. 원고 표현대로라면 이 문제는 "완전히 자동화된 방식으로 해결"됐다 . AI가 작성한 문제 진술이 내부 추론 모델로 전달됐고, 모델이 해법을 만들었으며, AI 채점 파이프라인이 높은 신뢰도를 보고했다. 사람이 논증을 읽기 전에 모두 벌어진 일이다 . 진지하게 봐야 할 자율성은 바로 이것이다. 프롬프트에 답하는 챗봇이 아니라, 스스로 문제를 제기하고 시도하고 사전 채점까지 한 폐쇄 루프다.

그 이후의 과정도 그만큼 중요하다. 채점 신호가 나온 뒤에야 OpenAI 연구자들과 외부 수학자들, 즉 Noga Alon, Thomas F. Bloom, W. T. Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, Melanie Matchett Wood가 증명을 검토하고, 검증하고, 다시 쓰고, 단순화하고, 강화했다 . 2026년 5월 20일 제출된 그들의 동반 노트 arXiv:2605.20695는 기계가 만든 반례를 사람이 소화한 버전이며, 실제로 대부분의 수학자들이 읽고 신뢰하는 산출물이다 . 모든 주요 설명에서의 틀은 대체가 아니라 협업이다. AI가 후보를 만들었고, 인간이 인증하고 개선했다.

"그 자체로 흥미롭다고 느낀 첫 AI 산출 결과입니다." — Daniel Litt, 수학자이자 동반 노트 공동 저자 (source: Understanding AI).

제품 관점의 해석에는 두 가지 공백을 두고 봐야 한다. 첫째, 모델 이름이 공개되지 않았다. 1차 원고는 어떤 내부 시스템이 이 결과를 냈는지 밝히지 않으며, 공개 출시 제품인 GPT-5, o3, ChatGPT 중 무엇과도 1차 출처에서 연결되지 않는다 . 출시된 제품 이름을 붙인 headline은 OpenAI가 공개한 범위를 넘어선 추정이다. 둘째, 과정은 재현 가능하지 않다. OpenAI는 샘플링 프로토콜, 계산 비용, 채점 파이프라인 내부, 학습 세부사항을 공개하지 않았다 . 결과물, 즉 Erdős의 거의 선형 추측에 대한 반례는 수학을 읽어 독립적으로 확인할 수 있지만, 그것을 만들어낸 발견 파이프라인은 그렇지 않다.

이 시스템들을 평가하는 구축자들에게 실용적인 교훈은 이 구분에 있다. 검증 가능한 산출물과 검증 불가능한 워크플로는 별개의 주장으로 다뤄야 한다. 프런티어 모델이 연구 수학에서 진짜 새롭고 유의미한 단계를 기여할 수 있다는 점은 이제 입증됐다 . 그러나 배포 가능한 반복적 자율 발견 엔진은 아니다. 적어도 OpenAI가 지금까지 보여준 것만으로는 그렇다. 인간의 framing과 검증은 이 결과에서 의례적인 절차가 아니라, 여전히 하중을 받치는 핵심 부분이다.

Sawin의 명시적 n^1.014와 그 지수가 뜻하는 것

Sawin의 명시적 하한은 정성적 반박을 측정 가능한 반박으로 바꿔 주는 숫자다. 프린스턴 수학자 Will Sawin은 동반 논문(arXiv:2605.20579, 2026년 5월 20일 제출 )을 올려, 단위 거리 쌍이 n1.014114개를 넘는 임의로 큰 n점 평면 집합을 구성했다 . OpenAI의 원고는 존재만 증명했다. 즉 무한히 많은 n에 대해 ν(n) ≥ n1+δ가 되는 어떤 절대상수 δ > 0이 있다는 사실은 보였지만, δ를 특정하지는 않았다 . Sawin의 논문은 같은 수론적 Golod–Shafarevich 장치에서 구체적이고 계산 가능한 값을 끌어내 δ ≈ 0.014를 제시한다.

0.014는 작아 보이지만, 약 80년 만에 처음 나온 하한 지수의 개선이다 . 중요한 것은 크기가 아니라 국면 전환이다. Erdős의 거의 선형 추측은 1 + O(1/log log n) 꼴의 지수를 허용했다. 이는 n이 커질수록 1로 수렴하므로, 선형보다 더해지는 “추가” 거듭제곱은 극한에서 사라진다 . 고정된 δ는 다르게 작동한다. n1.014는 충분히 큰 모든 n에 대해 선형 지수보다 일정한 간격을 유지한다. 어떤 고정된 양의 δ도 결국 모든 고정된 C에 대해 C/log log n을 넘기 때문에, 둘은 단지 숫자가 다른 것이 아니라 질적으로 다른 성장을 설명한다.

아래 표는 이 명시적 하한을 오랫동안 기준점이 되어 온 결과들과 나란히 놓은 것이다. 하한 지수와 상한 지수는 여전히 넓은 구간을 사이에 두고 있다. Sawin은 바닥을 올렸지만, Spencer, Szemerédi, Trotter가 1984년에 증명한 O(n4/3) 천장은 그대로다 .

결과유형n에 붙는 지수연도
Erdős 격자 구성하한1 + o(1) → 11946
OpenAI 모델(존재 증명)하한1 + δ, δ > 0 미지정2026
Sawin의 명시적 결과하한1.0141142026년 5월
Spencer–Szemerédi–Trotter상한4/3 ≈ 1.3331984

AI의 산출물이 수학 안으로 어떻게 흡수되는지 지켜보는 개발자들에게는 이 순서 자체가 교훈이다. 모델은 존재론적 돌파구를 제공했고, 며칠 안에 한 인간 수학자가 같은 대수적 재료를 사용해 그것을 검증 가능한 지수로 수치화했다 . 1.014와 1.333 사이의 간격은 여전히 열려 있으며, ν(n)의 정확한 점근값도 아직 알려져 있지 않다.

Lean 형식화와 증명 인증

An 80-year conjecture fell to AI. What was actually proved?

이 반증에 대해 완전하고 독립적으로 인증된 Lean 증명은 아직 없다. Google DeepMind의 Formal Conjectures 저장소에는 Erdős 문제 #90, OpenAI의 반증, Alon 등 저자들의 정성적 명제, 그리고 Sawin의 명시적 “1.014114” 변형이 기록되어 있다. 하지만 화면에 보이는 정리 본문에는 아직 Lean에서 증명되지 않은 목표를 표시하는 sorry 자리표시자가 남아 있다 . 따라서 이 파일은 기계 검증이 아니라 형식 명제 벤치마크에 가깝다.

이 차이는 이를 “AI가 검증한 수학”의 증거로 읽는 사람에게 중요하다. 현재 Lean 파일이 인증하는 것은 주장들이 형식화될 만큼 충분히 정밀하게 서술되어 있다는 점이다. 추측, 존재론적 하한, 명시적 지수는 각각 타입이 붙은 시그니처를 갖는다. 하지만 그 목표들을 해소하는 항은 아직 들어 있지 않다. sorry 토큰이 검증된 증명 항으로 대체되기 전까지, Lean은 인증 계층이 아니라 문제 서술 등록부로 기능하고 있다 .

현재 인증은 인간의 독해에 기대고 있다. 1차 출처는 통상적인 학술지 동료평가 밖에 있는 세 편의 프리프린트다. OpenAI의 CDN 호스팅 원고, Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang, Wood가 쓴 압축된 arXiv 노트 arXiv:2605.20695, 그리고 Sawin의 명시적 하한 논문 arXiv:2605.20579이며, 모두 2026년 5월 20일 날짜다 . 이 중 어느 것도 학술지 심사를 통과하지 않았다. 대부분의 수학자들이 신뢰할 만한 논증 버전으로 보는 것은 짧은 인간 검증 노트다.

커뮤니티의 장부도 이런 혼합 상태를 반영한다. Erdős Problems 데이터베이스는 이제 #90에 “DISPROVED (LEAN)”이라고 표시하고 500달러 상금을 적어 두었다. 본문에는 Erdős가 1982년에 n^(1+o(1)) 형태의 증명 또는 반증에 300달러를 걸었다고 적혀 있다 . “(LEAN)” 태그는 공식 증명이 아니라 기록된 형식 명제를 뜻한다. 이 반증은 전문가의 인간 독해로 검증되었고, 완전한 형식화는 아직 남아 있다는 점을 알려 주는 유용한 표시다.

결과를 어떻게 봐야 할까: 난해한 수학에서 AI가 잘하는 것과 아직 넘지 못한 경계

이 결과를 정직하게 읽으면, 최전선 추론 모델이 이미 가진 두 가지 성질, 즉 서로 동떨어진 하위 분야를 넓게 넘나드는 능력과 수많은 실패를 감수하며 밀어붙이는 끈기가 그대로 힘을 발휘한 사례다. 동시에 여전히 인간에게 전적으로 의존하는 부분도 뚜렷하게 드러난다. 진짜 진전은 대수적 수론(류체 타워, 완전 분해 소수, 민코프스키 격자)을 평면 결합 기하와 연결한 데 있었고, 이는 약 80년 동안 어떤 인간도 만들지 못했던 다리였다 . 분석가 Timothy B. Lee는 이를 정확히 짚었다. AI의 강점은 관련 없어 보이는 영역의 도구들을 폭넓게 탐색하고, 막다른 길의 "grind"를 버텨내는 데 있다. Jacob Tsimerman도 비슷한 수론적 접근을 시도했지만 시간이 너무 많이 든다고 보고 포기한 것으로 전해진다 .

실무자에게는 그 한계도 분명하며, 그대로 말해둘 필요가 있다:

  • 재현 가능한 경로가 없다. 1차 원고에서 내부 모델의 이름은 공개되지 않았고, OpenAI도 학습 세부 정보, 샘플링 프로토콜, 채점 파이프라인의 구체 내용, 계산 비용을 밝히지 않았다 . 오늘 어떤 API나 제품에 추측을 넣어 이 결과를 반복할 방법은 없다. 이 결과를 GPT-5, o3, ChatGPT와 연결하는 주장은 출처로 뒷받침되지 않는다.
  • 문제의 틀은 인간이 잡았다. 모델은 AI가 작성한 문제 설명을 받았다. 어떤 1946년 추측을 공략할 가치가 있는지 스스로 결정한 것이 아니다 .
  • 증명 검증도 인간이 했다. Noga Alon, W. T. Gowers, Will Sawin, Melanie Matchett Wood를 포함한 수학자들이 논증을 검증하고, 다시 쓰고, 단순화했다. Sawin은 별도로 명시적인 n1.014 경계를 추출했다 . 채점 파이프라인은 신뢰도를 표시했지만, 출판 가능한 논문을 만들어내지는 않았다.

이 역할 분담이 올바른 해석 틀이다. 끝에서 끝까지 자율적인 발명이 아니라 인간과 AI의 협업이다. Tim Gowers는 이 해법을 "a milestone in AI mathematics"라고 불렀고, Daniel Litt는 자신이 "exciting in itself"라고 느낀 첫 AI 산출 결과라고 설명했다 . 두 평가가 특히 주목할 만한 이유는 "진정으로 새로운" 결과라는 기준은 충족했지만, 검증 단계가 선택 사항이 되었다고 주장한 사람은 없었기 때문이다.

빌더에게 남는 구체적 교훈은 이렇다. 최전선 추론 모델은 연구 수학에서 검증 가능하고 새로운 한 단계를 기여했다. 약 δ ≈ 0.014의 하한 개선이며, 약 80년 만의 첫 개선이다 . 하지만 그 작업은 목표를 고르고 산출물을 점검한 인간의 틀 안에서 이루어졌다. 난해한 기술 작업에 AI를 평가하고 있다면, 문제 설정과 인증에는 전문가를 붙이고, 재현 불가능한 벤더 데모는 정확히 그 정도로 취급하며, 가치는 자율성 주장보다 검증된 단계로 측정해야 한다.

자주 묻는 질문

AI가 단위 거리 문제를 해결했나요?

아니요. 이 모델은 고정된 δ > 0에 대해, 무한히 많은 n에서 적어도 n1+δ개의 단위 거리 쌍을 갖는 평면 점 집합을 구성해 에르되시가 추측했던 거의 선형에 가까운 상한을 반박했습니다 . ν(n)의 정확한 점근 형태는 여전히 알려져 있지 않으며, Spencer, Szemerédi, Trotter가 1984년에 증명한 O(n4/3) 상한도 그대로 남아 있습니다 . 정확한 표현은 “추측을 반박했다”이지, “문제를 해결했다”가 아닙니다.

어떤 OpenAI 모델이 이 증명을 만들었나요?

OpenAI는 모델 이름을 밝히지 않았습니다. 주요 원고는 “내부 범용 추론 모델”이라고만 설명하며, 학습 세부사항, 샘플링 프로토콜, 계산 비용은 공개하지 않습니다 . 어떤 주요 출처에서도 GPT-5, o3, ChatGPT 같은 프로덕션 릴리스가 특정되지 않았으므로, 이 결과를 특정 제품명과 연결하는 주장은 근거가 없습니다 .

n^1.014 지수는 실제로 무엇을 뜻하나요?

이는 약 80년 만에 나온 단위 거리 하한 지수의 첫 개선입니다. Princeton의 Will Sawin은 n개 점으로 이루어진 평면 집합에서 n1.014114개보다 많은 단위 거리 쌍을 만드는 명시적 구성을 게시했습니다(arXiv:2605.20579, 2026년 5월 20일 제출) . 이전 구성의 지수는 n이 커질수록 1에 수렴했습니다(n1+c/log log n). 반면 1보다 큰 고정 지수는 질적으로 다릅니다. 점 집합이 커질수록 그 이점이 누적되기 때문입니다 .

이 증명은 Lean으로 형식 검증되었거나 동료 심사를 거쳤나요?

아직 둘 다 아닙니다. Google DeepMind의 Formal Conjectures 저장소에는 문제 #90, 그 반박, 그리고 Sawin의 명시적 “1.014114” 변형이 기록되어 있지만, 보이는 정리 본문에는 sorry 자리표시자가 들어 있습니다. 이는 형식 진술 벤치마크이지, 인증되고 독립적으로 확인 가능한 증명이 아닙니다 . 현재 이 결과는 arXiv 프리프린트와 OpenAI 원고 형태로 존재하며, 어느 것도 전통적인 학술지 동료 심사를 완료하지 않았습니다 . Erdős Problems 데이터베이스는 문제 #90을 “DISPROVED (LEAN)”로 표시하고 $500 상금을 기재하고 있습니다 .

오늘날 어려운 연구 문제에 추론 모델을 쓴다는 것은 무엇을 의미하나요?

최전선 추론 모델은 전문가의 문제 설정과 사후 검증이 결합될 때 수학에 실제로 새롭고 검증 가능한 기여를 할 수 있습니다. 하지만 처음부터 끝까지 자율적으로 증명을 발견하는 단계가 현재의 현실은 아닙니다. 이 결과 역시 사람이 문제를 설정하고, 출력을 검증하고, 출판 전에 AI의 논증을 단순화하고 강화하는 과정이 필요했습니다. Alon, Gowers, Sawin, Tsimerman, Wood 등 여러 연구자가 작성한 동반 arXiv 노트(arXiv:2605.20695)는 이를 소화해 사람이 검증한 버전으로 제시했습니다 . 빌더에게 가치는 자율성 주장보다 검증된 단계로 측정하는 편이 가장 좋습니다 .