2026년 11월 1일 (일).

핵심 요약

• 개발자가 로컬 LLM으로 프로그래밍 작업을 하도록 돕는 '코딩 하네스'를 직접 개발했다.
• 기존 도구들이 웹 스택 기반이라 수GB 메모리를 소비하는 문제를 해결하기 위해 C++와 Dear ImGui로 작성하여 기존 도구 대비 100배 적은 리소스를 사용한다.
• llama.cpp, OpenRouter, Anthropic API 등 외부 모델 제공자와 연동하며, 내장 모델 공급자는 없다.

핵심 요약

• 저자가 GPT-5.6 Sol 모델을 Codex에서 낮은 사고 수준으로 실행하여 13.5시간의 게임 시간으로 팩토리오 평화모드(생물 무적) 완주에 성공했다.
• 게임 매니저를 통해 모델이 Python 라이브러리를 사용해 프로그래밍 방식으로 게임을 플레이했으며, GUI 사용자와 동일한 제약(플레이어 도달 거리, 안개 기능)을 적용했다.
• 모델은 일부 영역에서는 기대를 초과했으나 명확한 약점도 보였고, 전체 런이 기록되어 해설 영상 제작 중이다.

핵심 요약

• Lean 개발자 Leo de Moura는 AI가 형식검증을 실용적으로 만들고 있으며, 코드 생성이 쉬워진 지금이 검증의 중요성이 높아진 순간이라고 주장한다.
• Lean은 프로그래밍 언어이자 정리증명기로, 코드의 성질을 명시하고 기계검증되는 증명을 작성할 수 있다. 신뢰하려면 Lean 커널만 믿으면 되고, 다중 커널이 존재한다.
• AI 기반 자동형식화(autoformalization)로 어떤 언어의 코드든 Lean 모델로 변환할 수 있게 됐다. 예로 Microsoft의 SymCrypt 암호화 라이브러리는 Aeneas 도구를 통해 Lean으로 검증된다.