긴 문맥보다 중요한 것은 오래 유지되는 구조와 검증이다

Claude 기반 다중 에이전트 시스템이 FLT를 Lean으로 기계검증 가능하게 옮겼다

첨부 문서는 Anthropic이 Claude 기반 multi-agent system으로 Fermat's Last Theorem의 최초 end-to-end computer-checked formalization을 Lean에서 완성했다고 공개한 내용을 핵심 변화로 제시한다. 작업은 약 11일 동안 진행되었고, 결과물은 약 1,300만 줄의 Lean 코드와 약 30,300개의 중간 정리 증명 규모이며, 수십 개 Claude agent가 병렬로 참여했다. 최종 correctness는 Lean kernel이 검증했다.

Wiles와 무관한 새로운 수학적 증명을 발견한 것은 아니다

원문은 이 경계를 매우 분명하게 긋는다. Claude가 Wiles 계열과 독립된 새로운 FLT 증명을 발견한 것이 아니다. 알려진 Wiles 계열 증명의 단순화된 전개를 기반으로 방대한 의존관계를 Lean에서 완전히 machine-checkable한 형태로 옮긴 autoformalization 성과이다.

agent들은 프로젝트 상태를 잃고 협업이 무너졌다

첨부 문서에 따르면 초기 시도에서는 여러 agent가 장기간 프로젝트 상태를 유지하지 못했고 coordination이 붕괴했다. 이는 단일 호출 수준에서 강한 추론 능력을 보여도, 작업이 수일 이상 이어지고 수많은 subproblem이 서로 의존하기 시작하면 상태 보존과 의존성 관리가 별도의 병목이 된다는 점을 드러낸다.

Theorem DAG가 memory와 decomposition을 동시에 담당한다

전환점은 Prove2Me라는 외부 scaffold였다. 전체 증명을 theorem DAG로 관리하고, 각 agent가 어떤 sub-theorem을 해결할지 결정하도록 하며, 자연어 설명과 형식정리를 연결해 검색과 재사용을 가능하게 했다. 문서는 Anthropic이 이 구조가 memory degradation과 multi-agent coordination 문제를 완화했다고 설명한다고 정리한다.

Long-horizon intelligence는 long context와 동일하지 않다

원문은 이 사례를 앞서 관찰한 “model + harness + persistent state” 방향과 같은 흐름으로 해석한다. 여기서 새롭게 선명해진 점은 persistent state가 단순 memory buffer가 아니라 구조화된 dependency graph라는 사실이다.

LLM judge 대신 Lean kernel이 correctness를 결정한다

일반적인 autonomous agent pipeline에서는 성공 여부를 다시 LLM judge가 평가하는 경우가 많다. 하지만 이 사례에서는 final correctness를 Lean kernel이 결정한다. 모델이 “맞다”고 주장하는 것과 artifact가 실제로 type-check되고 kernel validation을 통과하는 것은 완전히 다른 층이다.

외부 verifier는 실패를 단순 점수가 아니라 수정 가능한 오류 신호로 바꾼다. compile 또는 proof checking이 실패하면 어디에서 formal artifact가 무너졌는지 추적할 수 있고, agent는 그 오류를 국소적으로 수정한 뒤 다시 검증한다.

생성 능력보다 폐루프의 질이 더 중요해진다

좋은 hypothesis나 proof sketch를 한 번 생성하는 것만으로 장기 연구 자동화가 완성되지 않는다. 지속 가능한 시스템은 artifact를 만들고, 외부 verifier의 피드백을 받고, error localization을 수행하고, 상태 graph를 업데이트하면서 다시 시도해야 한다.

Foundation model은 핵심이지만 전체 시스템은 아니다

이 식은 AGI의 정의를 확정하는 공식이 아니라 첨부 문서가 최근 연구 방향을 구조적으로 정리한 synthesis이다. 이번 FLT formalization이 특히 새롭게 강화한 것은 Structured Task Graph + Deterministic Verification이다.

약점이 생길 때 모델을 다시 학습시키는 대신 외부 구조를 바꿀 수 있다

장기 작업이 무너지는 원인이 memory degradation이나 coordination이라면, 해법은 반드시 parameter update일 필요가 없다. task graph, harness, verifier, recovery logic 같은 model-external layer가 실패 모드를 흡수할 수 있다. 이 관점은 AGI 연구의 실험 단위를 model checkpoint에서 model + scaffold + persistent state + verifier의 조합으로 확장한다.

Hypothesis를 검증 가능한 artifact로 바꾸는 것이 핵심이다

첨부 문서는 self-improving agent와 Autonomous AI Scientist가 먼저 빠르게 발전할 가능성이 높은 영역으로 외부의 반증 가능한 verifier를 가진 분야를 지목한다. 수학은 Lean, 코드는 compiler/test suite, 알고리즘은 executable evaluator가 그 역할을 맡을 수 있다.

수일·수주 동안 유지되는 agent를 verification-first로 설계한다

첫 번째 연구축은 Verifier-Grounded Long-Horizon Agents이다. 장기 계획을 단순히 더 많은 context token으로 유지하는 대신, 외부 state representation과 verifier를 중심으로 progress를 축적한다. 핵심 metric도 단발 성공률에서 state persistence, recovery, verifier-confirmed progress로 확장할 수 있다.

기억을 저장소가 아니라 dependency-bearing working state로 본다

두 번째는 Graph-Structured Persistent Memory for AGI이다. theorem DAG처럼 node가 단순 정보 조각이 아니라 해결해야 할 subproblem, 이미 검증된 artifact, dependency, failure state를 함께 표현한다. memory와 planning을 별도 모듈로 나누기보다 하나의 evolving graph로 통합하는 접근이 장기 agent architecture의 중요한 방향이 될 수 있다.

자율 연구의 병목은 생성보다 검증 가능한 artifact interface일 수 있다

세 번째는 Machine-Checkable Autonomous Scientific Discovery이다. hypothesis를 검증 가능한 artifact로 변환하고, machine verifier가 failure를 돌려주며, agent가 그 결과로 belief와 artifact를 수정하는 closed loop를 구축한다.

성과를 크게 보되 증거의 범위를 넘지 않는다

이번 사례가 바꾼 질문은 ‘모델이 얼마나 똑똑한가’가 아니다

더 생산적인 질문은 이것이다. 충분히 좋은 모델에 어떤 scaffold와 verifier를 결합해야 장기적으로 상태를 잃지 않고, 오류를 확인하며, 수일·수주 동안 계속 진전할 수 있는가.

이 업데이트를 여섯 문장으로 압축하면