Chapter 1: 도입, 레시피 설정, 2단계 초반과 난항 (00:04-09:40)
- [00:17] Claude Code로 9개월 전에 했던 Lean 형식화 작업을 다시 해보겠다고 목표를 밝힌다.
- [00:23] Equational Theories Project의 특정 명제(Equation 1689 → Equation 2 함의)를 형식화하는 상황 설명.
- [00:46] 9개월 전에는 GitHub Copilot 등의 도움을 받아 단계별로 손으로 Lean 형식화를 했다고 회고.
- [01:17] 첫 번째 시도에서 Claude에게 “전체를 다 형식화해달라”고 한 번에 맡겼더니, 45분 돌다가 컴퓨터가 다운되고 토큰도 떨어졌다.
- [01:32] 두 번째 시도에서는 단계별로 요청했고, 약 25분 만에 완전한 증명을 얻었다.
“[02:01] Claude에게 좋은 지침을 주는 것이 도움이 된다는 것입니다.”
- [02:07] 이번 작업을 위한 단계별 “레시피”를 적어두기로 결정. S/F 표기법 도입, Lemma 1·2·3 순서대로 진행.
- [04:02] 각 명제를 형식화하되 이 단계에서는 증명하지 말라고 지침. 한 번에 다 하면 보조정리 증명에서 막혀 아무것도 못 하게 된 경험 반성.
- [05:02] 최선의 관행은 “지침을 담은 마크다운 파일”을 만들어 제공하는 것이라고 조언.
- [05:29] 보조정리들의 진술이
sorry로 채워져 있지만, 적어도 진술 자체는 제대로 됐다고 확인. - [06:37] 라인 단위로 만들어두면 “무슨 일이 일어나는지에 대한 정보/감각”을 덜 잃게 된다고 강조.
- [08:31] 증명의 하위 수준 단계들에서 백트래킹이 발생하며 토큰을 많이 소모.
- [09:07] 하위 수준이 가장 쉬울 거라고 생각했는데 오히려 가장 어려운 부분이어서 놀랍다고 반응.
Chapter 2: 레마 2/3 뼈대 요청, 다운/복구, 디버깅과 병렬 편집 (10:06-19:58)
- [10:06] 레마 2에 대해서는 증명의 “뼈대”를 잡아 달라고 요청하는 전략. 이전에도 뼈대 잡기를 잘했기 때문.
- [10:45] 레마 2는 뼈대를 받으면 본인이 빈칸을 손으로 채우겠다는 분업 방식 제안.
- [11:04] 메인 컴퓨터가 다운되어 잠깐 멈추고 복구.
- [11:19] 단계별로 진행하면 예상치 못한 일이 생겨도 “다시 이어서 하기가 더 쉽다”는 장점.
- [12:42] 손으로 하는 것보다 “그리 많이 빠르지는” 않지만, 자율적으로 돌아가니 다른 일을 할 수 있다는 장점.
- [13:50]
ssa가 두 번 나타나며 첫 번째만 펼쳐야 하는 디버깅 문제 발견. 합동식에서 같은 항을 소거하는 방법으로 해결. - [15:45] 소거 전술이 “너무 강력해서 그냥 됐다”며 의도보다 쉽게 해결.
- [17:34]
h1을 독립된 레마로 뽑아내면 여러 항목을 같은 레마로 증명할 수 있다는 전략. - [19:04] 사람이 다른 걸 편집 중이어도 Claude가 독립적으로 편집을 진행해주는 점이 좋다.
“[19:25] 음, 저는 병렬로 이 에이전트와 함께 작업할 수 있다는 점에 만족합니다.”
- [19:37] 계속 관여하면서 “고르고 선택”하는 방식이 핵심 워크플로. 이해한 부분은 에이전트에게 맡긴다.
- [19:58] 여러 에이전트를 동시에 돌리는 방식도 있지만, 본인은 에이전트 하나로도 충분히 만족.
Chapter 3: 스케일링, 남은 문제 수정, 자동화의 트레이드오프 (20:11-24:19)
- [20:11] 여러 에이전트 관리는 정신적 자원이 너무 많이 들어서 과하다고 평가.
- [20:57] 에이전트가 각 단계를 어떻게 형식화할지 알아낸 것 같다고 확인.
- [21:46] 형식화된 내용이 비형식적 증명과 잘 맞는지 대조 점검. 사람이 같은 논증을 형식화할 때의 방식과 비슷.
- [22:27] 자동화가 강해지면 “뇌를 꺼 버리고” 에이전트에게 맡기고 싶어지는 유혹이 있지만, 중간 개입을 계속해야 한다.
“[22:52] 많이 의존하다가 뭔가가 잘못되면 여러분은 그냥 뭘 해야 할지 전혀 모르고,”
- [22:56] 과의존하면 문제가 생겼을 때 “계속 반복 호출”하는 것밖에 할 수 없게 된다고 경고.
- [23:02] 형식 증명을 비공식 증명과 잘 맞춰두면 읽고 디버그하기가 훨씬 쉬워진다.
- [23:11] 형식화를 통째로 맡기면 에이전트가 비공식 증명을 무시하고 자기 방식으로 해버릴 수 있어 위험.
- [24:05] 여전히 본인이 “꽤 많이 생각”하고 있다며, 완전 자동화/무사고 상태는 아니라고 선을 긋는다.