어릴 때 즐겨보던 TV 쇼가 내 엔지니어링 커리어의 기초가 되었다면 믿으시겠습니까? PBS Kids의 Cyberchase는 많은 아이들에게 수학적 사고방식의 씨앗을 심어준 전설적인 프로그램입니다. 그런데 최근 Hacker News에서 아주 흥미로운 글을 발견했습니다. 바로 이 어린이 만화의 에피소드를 Lean4 라는 정리 증명기(Theorem Prover)를 사용해 수학적으로 검증한 프로젝트입니다.

솔직히 처음엔 “굳이?”라는 생각이 들었습니다. 하지만 글을 읽어내려가며, 이것이 단순한 장난감이 아니라 우리가 매일 씨름하는 분산 시스템의 정합성 검증 과 본질적으로 같다는 것을 깨달았습니다. 오늘은 이 프로젝트를 통해 현대적인 Formal Verification(형식 검증)이 어디까지 왔는지, 그리고 이것이 우리 같은 시니어 엔지니어들에게 어떤 의미가 있는지 뜯어보겠습니다.

왜 SMT Solver가 아니라 Lean인가?

우리는 보통 복잡한 로직을 검증할 때 Z3 같은 SMT Solver를 떠올립니다. 하지만 원문 저자가 지적했듯, SMT Solver는 강력하지만 때로는 “블랙박스” 같습니다. 휴리스틱에 의존하고, 가끔은 버그가 있기도 하죠.

반면 Lean 은 Interactive Theorem Prover입니다. 수학적 사실(Fact)들을 쌓아올려 가장 낮은 레벨의 공리(Axiom)까지 증명합니다. 컴파일러가 타입 체크를 통과시키면, 그 논리는 참인 것입니다. AWS의 Automated Reasoning 그룹이 이 분야에 투자를 많이 하고 있는데, 그 이유가 있습니다. “버그 없음”을 확률이 아니라 논리로 보장 하고 싶기 때문입니다.

Cyberchase의 님(Nim) 게임 모델링

검증 대상은 간단합니다. 15마리의 용(녹색 14, 빨강 1)이 있고, 두 팀이 번갈아 가며 1~3마리를 가져갑니다. 빨간 용을 가져가는 팀이 집니다. 전형적인 님(Nim) 게임 의 변형이죠.

Lean에서의 모델링은 함수형 프로그래밍과 수학의 중간 지점에 있습니다. 여기서 흥미로운 엔지니어링 챌린지가 발생합니다. 바로 상호 재귀(Mutual Recursion)와 종료(Termination) 문제 입니다.

mutual
  def squadWins (green_dragons: Nat): Bool :=
    if green_dragons = 0 then False
    else ¬ hackerWins (green_dragons - (squadStrategy green_dragons))

  def hackerWins (green_dragons: Nat): Bool :=
    if green_dragons = 0 then False
    else ¬(squadWins (green_dragons - 3)) ∨ ...
end

코드를 이렇게 짜면 Lean은 에러를 뱉습니다. “이 함수가 끝난다는 걸 어떻게 보장해?”라는 거죠. 우리도 현업에서 재귀 함수를 짤 때 무한 루프를 걱정하지만, Lean은 이걸 증명 하라고 요구합니다. 결국 green_dragons의 숫자가 줄어든다는 것을 명시적으로 증명해야 컴파일이 됩니다. 이 엄격함이 귀찮게 느껴질 수도 있지만, Mission Critical 시스템에서는 이런 엄격함이 생명줄입니다.

‘Sorry’ 주도 개발과 강력한 전술(Tactics)

이 글에서 가장 마음에 들었던 부분은 sorry 키워드의 활용입니다. Lean에서 sorry는 “이건 나중에 증명할게, 일단 넘어갑시다”라는 뜻입니다. 일종의 Proof by Laziness 인데, 우리가 인터페이스만 먼저 정의하고 구현을 나중에 하는 것과 비슷합니다.

증명 과정에서 저자는 rw (rewrite), simp (simplify) 같은 전술(Tactics)을 사용합니다. 특히 omega라는 전술이 인상적입니다. 이건 단순한 부등식이나 모듈러 연산을 자동으로 증명해주는 툴입니다. 주니어 개발자가 “이거 계산하면 맞습니다”라고 보고하는 대신, 수학적으로 완벽한 계산기가 증명 단계를 채워주는 셈입니다.

-- ⊢ green_dragons % 4 > 0
omega

이 한 줄로 복잡한 산술 증명이 끝납니다. omega가 내부적으로 생성한 증명 단계들 역시 Lean 커널에 의해 검증되므로 안전합니다. 400줄이던 코드가 75줄로 줄어든 비결이 바로 이런 강력한 자동화 도구들 덕분입니다.

독이 든 숫자 (Poison Number)와 귀납법

결국 이 게임의 필승 전략은 (n % 4)만큼 가져가서 상대방에게 4의 배수(Poison Number)를 남기는 것입니다. 이를 증명하기 위해 강한 귀납법(Strong Induction) 을 사용합니다.

induction green_dragons using Nat.strongRecOn with
| _ green_dragons hd => ...

이 과정에서 저자는 mod_zero_plus_k라는 커스텀 정리를 만들어 사용합니다. (x + k) % n = k임을 증명하는 것인데, Mathlib(Lean의 표준 라이브러리)에 없어서 직접 구현했다고 합니다. 이런 부분이 Formal Verification의 진입장벽이면서 동시에 매력입니다. 필요한 도구가 없으면 수학적 공리로부터 직접 만들어내야 합니다.

Hacker News의 반응: 기술은 여전히 재미있는가?

이 글과 관련된 Hacker News 스레드에서는 2000년대 초반의 기술 교육에 대한 향수가 터져 나왔습니다. 한 유저는 “요즘엔 아이들을 위한 AI 테마의 쇼가 없다. 기술이 더 이상 탐험의 대상이 아니라 착취적인(extractive) 도구가 되었기 때문”이라고 한탄하더군요.

하지만 반대 의견도 만만치 않았습니다. “라즈베리 파이, 로보틱스 등 지금이 기술을 배우기에 훨씬 더 좋은 환경이다. 단지 LLM으로 시작하게 하지 말고, 스스로 탐구하게 놔두면 된다”는 의견에 저도 동의합니다.

Lean으로 게임을 검증하는 이 과정 자체가 바로 순수한 탐구 의 결정체입니다. AI가 코드를 짜주는 시대에, 가장 기초적인 논리부터 쌓아올려 “참”임을 증명하는 행위는 엔지니어로서 잃어버린 야성을 되찾아주는 느낌이 듭니다.

결론: Production 레벨인가?

아직 Lean을 당장 내일의 마이크로서비스 비즈니스 로직 검증에 도입하라고 권하긴 어렵습니다. 학습 곡선이 에베레스트산만큼 가파르기 때문입니다. 하지만 분산 데이터베이스의 합의 알고리즘 이나 컴파일러 최적화 같은 핵심 코어 로직을 다루는 엔지니어라면, TLA+와 함께 Lean을 눈여겨봐야 합니다.

“테스트는 버그가 있음을 보여줄 수 있지만, 버그가 없음을 보여줄 수는 없다”는 다익스트라의 말은 여전히 유효합니다. 하지만 Lean 같은 도구가 발전하면서, 우리는 언젠가 “버그가 없음”을 수학적으로 보장하는 코드를 작성하는 날을 맞이할지도 모릅니다. 400줄이 75줄이 된 것처럼, 그 미래는 생각보다 빨리 다가오고 있습니다.

참고 자료:

• Formally Verifying PBS Kids with Lean4
• Hacker News Discussion