26:29
Claude Code를 사용해 Lean에서 증명 형식화하기
- 9개월 전 형식화 작업을 Claude Code로 다시 수행하며, 한 번에 맡기기보다 단계별 레시피가 중요하다고 정리한다.
- S/F 표기 도입 → 골격 만들기 → 줄 단위 변환/뼈대 요청 → 막히는 지점 수동 디버깅까지, 사람-에이전트 병렬 워크플로를 실험한다.
- 자동화의 유혹과 과의존 리스크를 경계하며, 비공식 증명과의 정렬 및 중간 개입이 읽기/디버깅에 핵심이라고 강조한다.