Opus 4.6은 Lean으로 범주론을 할 수 있습니까?

2026년 2월 16일 · 태그: ai, mathematics, formal-methods · 원문 · 한국어 번역(원문에서 변경됨)

저는 약 10년 동안 이리저리 옮겨 다니며 다듬어 온 작은 범주론 라이브러리를 하나 가지고 있습니다. 이 라이브러리는 Haskell에서 시작하여 Agda로 포팅되었고, 잠시 Idris에 머물렀다가, Coq에서 얼마간 시간을 보낸 뒤, 이제 Lean 4에 자리 잡았습니다. 저는 이것을 Kitty Cats라고 부릅니다. 아이디어는 간단합니다. Awodey의 Category Theory와 Mac Lane의 Categories for the Working Mathematician 중 관련 장에 나오는 정의와 정리를 가져와서, 타입 검사가 가능한 코드로 직접 옮기는 것입니다. 범주, 함자, 자연 변환, 곱, 극한, 수반, 모나드, 요네다 보조정리입니다. 라이브러리도 없고, 직접 정의한 것 외에는 어떤 import도 없습니다. 모든 것을 마치고 나면 Lean 코드로 약 900줄 정도입니다. 이것은 머릿속에 통째로 담을 수 있는 종류의 프로젝트이며, 바로 그 점이 핵심입니다. 새로운 의존 타입의 언어나 증명 보조기가 나올 때마다, 저는 이 뼈대를 꺼내 들고 그것이 어떤 느낌인지 살펴봅니다. 이것은 저의 리트머스 시험이자, 표준 연습 문제이며, 무인도에 가져갈 단 하나의 형식화입니다. 그리고 이것은 언어 모델이 추상적이고 형식적인 “추론“을 얼마나 잘하게 되었는지(어쩌면 그저 그것을 흉내 내는 것일 수도 있지만, 그 질문은 철학자들에게 맡기겠습니다!)를 가늠하는 좋은 벤치마크가 점점 더 되어 가고 있습니다.

그래서 Anthropic이 새로운 Opus 4.6 모델을 내놓았을 때, 저는 이것이 실제로 제대로 된 Lean 4를 작성할 수 있는지 알고 싶었습니다. 장난감 예제가 아닙니다. theorem two_plus_two : 2 + 2 = 4 := rfl 같은 것도 아닙니다. 실제 증명 의무를 지닌 실제 증명, 즉 자연성 사각형과 정합 조건을 붙들고 씨름해야 하고 엘라보레이터가 매 단계마다 발목을 잡는 바로 그런 카인드의 증명입니다. 증명 보조기의 아름다운 점은 답을 근본적으로 검증할 수 있다는 것입니다. 출력물을 가늘게 뜬 눈으로 들여다보며 미묘하게 틀린 곳이 있지 않은지 고민할 필요가 없습니다. lake build가 통과하거나, 통과하지 않거나 둘 중 하나입니다. 커널은 여러분의 감정 따위에 신경 쓰지 않습니다.

짧게 답하자면, 네, 대체로 그렇습니다. 하지만 긴 답이 더 흥미롭습니다.

우리(저와 모델을 아우르는 장엄 복수형 “우리”)는 30분짜리 세션 두 번에 걸쳐 라이브러리 전체를 함께 만들었습니다. 기본 계층 구조는 빠르게 세워졌습니다. 범주, 함자, 자연 변환, 반대 범주, 사상 클래스입니다. 이것들은 대부분 증명 의무가 간단한 구조체 선언입니다. 범주 공리 $\mathrm{id}\circ f=f$, $f\circ \mathrm{id}=f$, $(f\circ g)\circ h=f\circ (g\circ h)$와 함자 법칙 $F(\mathrm{id})=\mathrm{id}$, $F(f\circ g)=F(f)\circ F(g)$가 그것입니다. Opus는 이것들을 땀 한 방울 흘리지 않고 처리했으며, 솔직히 말해 지금 시점에서는 웬만한 언어 모델이라면 대부분 그렇게 할 것입니다. 증명은 한두 개의 전술로 이루어지며, 대개 rfl이나 by simp면 충분합니다. 진짜 질문은 언제나 증명이 어려워질 때 어떤 일이 일어나는가였습니다.

모노이드 범주와 자기 함자 구성에 이르러 상황이 흥미로워졌습니다. 자기 함자의 범주가 합성에 대해 모노이드 범주임을 증명하려면, 오각형 정합성 조건과 삼각형 정합성 조건을 확립해야 합니다. 오각형 공리는 네 겹 텐서곱을 재결합하는 두 가지 방법이 일치한다는 것을 말합니다:

$$({\alpha }_{F,G,H}\otimes {\mathrm{id}}_K)\circ {\alpha }_{F,G\circ H,K}\circ ({\mathrm{id}}_F\otimes {\alpha }_{G,H,K})={\alpha }_{F\circ G,H,K}\circ {\alpha }_{F,G,H\circ K}$$

여기서 $\alpha$는 결합자 자연 동형입니다. 삼각형 공리는 결합자를 왼쪽 및 오른쪽 단위자 $\lambda$, $\rho$와 연관 짓습니다:

$${\alpha }_{F,\mathrm{Id},G}\circ ({\mathrm{id}}_F\otimes {\lambda }_G)={\rho }_F\otimes {\mathrm{id}}_G$$

이것들은 바로 형식화하기 성가신 종류의 것입니다. 목표에 수평과 수직으로 합성된 깊이 중첩된 자연 변환이 들어 있고, 무엇이 “정의상 같은지“에 대한 엘라보레이터의 관념이 여러분의 직관과 항상 일치하지는 않기 때문입니다. Opus는 구조를 올바르게 잡을 수 있었고, 모노이드 범주 사영을 구체적인 NatTrans 표현으로 펼치는 show 블록을 세울 수 있었으며, 적절한 펼침 보조정리와 함께 ext a; simp [...]를 쓰면 목표가 닫힌다는 것도 알아낼 수 있었습니다. 하지만 Opus가 만들어 낸 증명은 장황했습니다. 중첩된 괄호의 벽이었습니다. 기술적으로는 옳지만 보고 있으면 눈이 풀려 버리는 종류의 것이었습니다.

이 라이브러리의 백미는 monadIsMonoidObj, 즉 모나드가 자기 함자 범주의 모노이드라는 증명입니다. 함수형 프로그래머라면 누구나 들어 본 농담이지만(이제는 밈이 되었을 정도입니다), 실제로 이를 형식화하려면 두 단계의 추상화를 이어야 합니다. 범주 $\mathcal{C}$ 위의 모나드 $(T,\eta ,\mu )$는 결합 법칙과 단위 법칙을 만족하는 자연 변환 $\eta :\mathrm{Id}\Rightarrow T$(단위)와 $\mu :T^2\Rightarrow T$(곱셈)를 갖춘 자기 함자 $T$입니다:

$$T({\mu }_a)\circ {\mu }_a={\mu }_{T(a)}\circ {\mu }_{a}T({\eta }_a)\circ {\mu }_a=\mathrm{id}{\eta }_{T(a)}\circ {\mu }_a=\mathrm{id}$$

이것들은 $\mathcal{C}$의 각 대상 $a$마다 하나씩 있는 성분별 등식입니다. $(T,\mu ,\eta )$가 모노이드 범주 $(\mathrm{End}(\mathcal{C}),\circ ,\mathrm{Id})$의 모노이드 대상을 이룬다는 것을 보이려면, 이 등식들을 자기 함자 범주에서의 자연 변환 등식으로 끌어올려야 하는데, 이 범주 자체가 방금 구축한 모노이드 구조를 갖추고 있습니다. MonoidObj 구조의 각 필드에는 모노이드 범주 사영을 수동으로 펼치는 show 블록이 필요하고(ext가 Hom 타입 별칭을 꿰뚫어 필요한 NatTrans를 찾지 못하기 때문입니다), 이어서 성분으로 환원하는 ext; endo_simp, 그다음 exact M.mul_assoc a 또는 해당하는 모나드 공리가 따라와야 합니다. Opus는 이 형태를 올바르게 잡았지만, 분해 방식에 대해서는 상당한 안내가 필요했습니다. 원래 출력에는 show 블록이 인스턴스 선언 안에 바로 인라인되어 있었는데, 깊이 중첩된 NatTrans.vcomp (endoTensorHom M.mu (NatTrans.ident M.T)) M.mu = ...가 서너 줄씩 이어져 있어서, 옳기는 해도 코드를 처음 읽는 사람이라면 누구든 겁에 질릴 만했습니다.

바로 이 지점에서 모델이 몇 가지 난관에 부딪혔고 도움이 필요했습니다. 우리는 증명을 리팩터링했습니다. 성분별 등식을 NatTrans 등식으로 끌어올리는 작은 도우미인 endo_ext_eq를 도입하여, show; ext a; endo_simp; exact로 이어지는 춤 대신 endo_ext_eq fun a => by endo_simp; exact M.mul_assoc a라고 쓸 수 있게 했습니다. 모노이드 정합성 의무를 독립된 보조정리(endoPentagon, endoTriangle, endoTensor_id, endoTensor_comp)로 추출하여 인스턴스 선언이 순수한 대입이 되도록 했습니다. 정리 시그니처에서 let 바인딩을 사용해 오각형 공리에 나오는 다섯 가지 결합자 인스턴스에 이름을 붙였고, 그 결과 (endoAssociator F (CFunctor.compose G H) K).hom의 벽이 읽기 쉬운 alpha_F_GH_K로 바뀌었습니다. monadIsMonoidObj 정의는 22줄의 인라인 증명에서 7줄의 이름 붙은 보조정리 적용으로 줄어들었습니다. 저는 이런 종류의 리팩터링이야말로 여전히 인간이 확실히 더 잘하는 일이라고 생각합니다. 독자가 무엇을 보아야 하는지 아는 것, 어떤 하위 표현식에 이름을 붙일 가치가 있는지 아는 것, 증명이 올바르기는 하지만 아직 좋지는 않은 때를 아는 것이 바로 그것입니다.

요네다 보조정리는 기분 좋은 놀라움이었습니다. 그 명제는 임의의 함자 $F:{\mathcal{C}}^{\mathrm{op}}\to \mathbf{Set}$과 $\mathcal{C}$의 임의의 대상 $a$에 대해 다음과 같은 자연스러운 전단사가 존재한다는 것입니다:

$$\mathrm{Nat}(\mathrm{Hom}(-,a),;F);\cong ;F(a)$$

정방향(자연 변환을 ${\mathrm{id}}_a$에서 평가하면 그것을 결정하는 원소가 복원됨)은 map_id만 있으면 거의 자명합니다. 역방향(${\mathrm{id}}_a$에서의 값으로부터 변환을 다시 구성함)은 자연성 등식을 추출하고, 그것을 단순화한 뒤, 대칭적으로 적용해야 합니다. Opus는 hom 집합이 Type 범주의 함수 타입일 때 필요한 약간 까다로운 congrFun 적용까지 포함하여 이를 올바르게 헤쳐 나갔습니다. 충실충만한 임베딩(yoneda_map_eval과 yoneda_eval_map)은 자연스럽게 따라 나왔습니다. 솔직히 조금 매료되었습니다.

이 작업이 이만큼 잘 된 것은 도구 덕분이었습니다. 여기서 두 오픈 소스 프로젝트의 공을 인정해야 합니다. Oliver Dressler가 만든 lean-lsp-mcp 서버는 Lean 4 언어 서버를 MCP 인터페이스로 노출하여, Claude가 목표 상태, 진단, 자동 완성, 호버 정보에 직접 접근할 수 있게 합니다. Cameron Freer가 만든 lean4-skills 플러그인은 그 위에 더 높은 수준의 증명 명령, 사이클 엔진, 전제 검색 통합을 더합니다. 이 둘이 함께 모델에게 진정한 피드백 루프를 제공합니다. 모델은 lean_goal을 호출하여 임의의 줄에서 증명 상태를 살펴보고, lean_diagnostic_messages를 호출하여 파일에 오류가 있는지 확인하고, lean_multi_attempt를 호출하여 여러 전술 시퀀스를 시도해 어느 것이 진전을 이루는지 확인하고, lean_run_code를 호출하여 작업 중인 파일을 수정하지 않고 완전한 코드 조각을 커널에 대해 시험해 볼 수 있습니다. 이는 작업의 역학을 근본적으로 바꿉니다. Lean 코드를 생성하고 컴파일되기를 바라는 대신, 모델은 증명을 작성하고, 목표 상태를 확인하고, 오류를 보고, 수정하는 촘촘한 루프 안에서 작동합니다. 눈을 가리고 그림을 그리는 것과 눈을 뜨고 그림을 그리는 것의 차이입니다. 모델은 여전히 실수를 하고, 적용되지 않는 전술을 시도하고 맞지 않는 rw 체인을 작성하기도 하지만, 이러한 실패를 즉시 감지하고 복구할 수 있습니다. 6개월 전에는 이런 종류의 통합이 존재하지 않았습니다. 그때라면 모델은 엘라보레이터가 만족하는지 비명을 지르는지 알 길도 없이 허공에 대고 Lean 코드를 생성하고 있었을 것입니다.

검색 도구도 중요합니다. lean_leansearch, lean_loogle, lean_leanfinder를 사용하면 모델이 자연어, 타입 시그니처, 의미적 유사성으로 Mathlib의 보조정리 데이터베이스를 조회할 수 있습니다. 이 프로젝트에서는 Mathlib을 사용하지 않았지만(처음부터 직접 구축하는 것이 핵심이므로), 보조정리 이름을 사용하기 전에 그 이름이 존재하는지 확인하거나, 존재해야 한다고 알고 있는 정리의 정확한 이름을 찾는 능력은 매우 귀중합니다. lean_state_search와 lean_hammer_premise는 한 걸음 더 나아가, 증명 상태가 주어지면 목표를 닫을 수 있을 법한 보조정리를 제안합니다. 이것이 바로 가장 강력한 자동 정리 증명기를 움직이는 기법인 전제 선택(premise selection)이며, 이를 API 호출 하나로 사용할 수 있습니다. “오각형 공리를 증명하라“라고 말하고 자리를 떠도 되는 수준에 아직 완전히 도달하지는 않았습니다. 그러나 적절한 안내만 있으면 상당히 많은 비자명한 정리 증명을 처리할 수 있는 수준에 놀라울 만큼 가까워졌습니다.

한계에 대해 솔직하게 말하자면, Opus는 복잡한 증명 상태를 작업 기억에 담아 두고 여러 단계를 앞서 계획해야 하는 종류의 추론에 어려움을 겪습니다. 단일 전술이나 짧은 체인으로 풀리는 목표는 닫을 수 있지만, 자연성 방정식을 도입하고, 그것을 특정한 방식으로 단순화한 다음, 긴 합성 체인의 특정 위치에 적용해야 하는 다단계 재작성은 여전히 일일이 이끌어 주어야 합니다. 때로는 rw가 필요한 곳에서 simp를 시도하거나, 보조정리를 잘못된 위치에 적용하거나, ext가 작동하려면 show 블록이 필요하다는 사실을 잊어버리기도 합니다. 이는 이해의 근본적인 실패가 아니며, 오히려 대학원생이 증명 보조기를 처음 접한 첫 학기에 저지르는 실수에 가깝습니다. 모델은 무엇을 증명하고 싶은지 알고 전략도 대략 알고 있지만, 엘라보레이터의 동의를 얻어 내는 번거로운 세부 사항을 처리하려면 반복이 필요합니다.

한 가지 짚어 둘 만한 점이 있습니다. 비공식적인 실험에서 추론 예산을 늘리자 수렴 시간은 실제로 늘어났지만(전술을 확정하기 전에 숙고하는 데 더 많은 토큰을 소비했기 때문입니다), 최종 출력의 품질이 눈에 띄게 향상되지는 않았습니다. 모델은 더 오래 생각하고도 결국 똑같은 simp 호출을 꺼내 들곤 했습니다. 이 과정은 비결정적이고 프롬프트에 매우 민감하기 때문에 경험적으로 측정하기 어려운 부분이므로, 걸러서 들으시기 바랍니다. 하지만 제 작업 가설은, 전술 수준의 정리 증명에서 병목은 “더 열심히 생각하는 것“보다는 루프 안에 적절한 도구 호출을 갖추는 데 있다는 것입니다. 내부의 사고 사슬보다 언어 서버의 피드백이 더 중요합니다.

문제는 지난 6개월 동안 이것이 기하급수적으로 나아졌다는 점입니다. 저는 이와 같은 실험을 주기적으로 해 왔는데, 그 발전 궤적은 놀라울 정도입니다. 1년 전만 해도 언어 모델은 문법적으로 올바른 Lean 코드조차 겨우 작성하는 수준이었습니다. 6개월 전에는 간단한 전술 증명은 처리할 수 있었지만, 유니버스 다형성이나 타입 클래스 해석이 관련된 문제에서는 무너지고 말았습니다. 오늘날에는 MCP 통합과 언어 서버 피드백 덕분에 두 번의 세션만으로 900줄 분량의 형식화된 범주론을 구축했으며, 여기에는 많은 수학 대학원생도 어렵게 느낄 만한 증명들이 포함되어 있습니다. 이것이 어디로 향하고 있는지 예측하기는 어렵지 않습니다.

그리고 어쩌면 그것이 흥미로운 부분일지도 모릅니다. AI가 오늘날 정리를 증명할 수 있다는 점(도움을 받으면 어느 정도는 가능합니다)이 아니라, 상투적인 보일러플레이트가 사라지고 있다는 점 말입니다. 형식화의 지루한 부분들, 즉 정합성 조건, 자연성 보조정리, simp 설정 같은 것들이야말로 언어 모델이 점점 잘하게 되는 구조화되고 검증 가능하며 기계적으로 확인할 수 있는 종류의 작업입니다. 이 층위가 사소해지면, 우리는 정말로 중요한 부분에 시간을 쓸 수 있게 됩니다. 올바른 추상화를 선택하고, 구조들 사이의 연결을 발견하고, 애초에 무엇을 형식화할 가치가 있는지 결정하는 일 말입니다. 증명 보조기는 관료적인 장애물이라기보다 진정한 사고의 도구가 되어 갑니다. 우리는 더 높이 쌓아 올릴 수 있게 됩니다.

저는 이 작은 범주론 라이브러리를 10년 동안 이 언어에서 저 언어로 옮겨 가며 가지고 다녔는데, 그때마다 그 경험은 저에게 기술의 현주소에 관해 무언가를 알려 주었습니다. 이번에 그것이 알려 준 것은 우리가 미래에 살고 있으며, 그 미래는 제가 예상했던 것보다 더 기묘하고 더 흥미롭다는 사실입니다.