드래그 앤 드롭으로 수학 증명을? 브라우저에서 논리학 배우는 '인크레더블 프루프 머신'

수학 증명을 퍼즐 게임처럼 푼다고요?

"증명"이라는 단어만 들어도 머리가 지끈한 분들 많으실 거예요. 대학교 이산수학 시간에 만났던 그 증명 말이에요. 그런데 이걸 드래그 앤 드롭 퍼즐 게임으로 바꿔버린 프로젝트가 있어요. 'The Incredible Proof Machine'이라는 웹사이트인데요. 설치도 회원가입도 필요 없이 브라우저에서 바로 실행되고, 논리 기호를 하나도 몰라도 시작할 수 있어요. 2016년에 만들어진 프로젝트인데 지금 봐도 신선하고, 오히려 형식 검증이 주목받는 요즘 다시 꺼내볼 가치가 커졌어요.

어떻게 동작하냐면

화면에는 블록들이 놓여 있어요. 각 블록은 하나의 '추론 규칙'이에요. 이게 뭐냐면, "A가 참이고 B가 참이면, 'A 그리고 B'도 참이다" 같은 논리의 기본 법칙 하나하나를 부품으로 만든 거예요. 왼쪽에는 주어진 가정(전제)이 있고, 오른쪽에는 도달해야 할 결론이 있어요. 플레이어가 할 일은 블록들을 선으로 연결해서, 가정에서 출발해 결론까지 이어지는 파이프라인을 만드는 거예요. 공장 자동화 게임 Factorio에서 컨베이어 벨트를 잇는 느낌과 비슷하다고 보시면 돼요.

재미있는 건, 이게 겉모습만 게임이 아니라는 거예요. 뒤에서는 '자연 연역(natural deduction)'이라는 진짜 논리학 체계가 돌아가고 있거든요. 자연 연역이 뭐냐면, 수학자들이 실제로 증명을 쓸 때 사용하는 사고 과정을 형식화한 규칙 체계예요. 그러니까 여러분이 블록을 연결해서 퍼즐을 풀면, 그건 장난이 아니라 논리학 교과서에 실어도 되는 엄밀한 증명을 완성한 거예요. 연결이 올바르면 뒤에서 돌아가는 검증기가 "이 증명은 유효합니다"라고 확인해주고요. 앞부분은 '그리고', '또는', '만약 ~라면' 정도만 다루는 명제 논리로 시작해서, 뒤로 가면 ∀(모든), ∃(존재한다) 기호가 나오는 술어 논리까지 이어져요. 난이도 곡선이 게임처럼 잘 설계되어 있어서, 어느 순간 자기도 모르게 꽤 어려운 증명을 하고 있게 돼요.

업계 맥락: 증명 보조기의 세계로 가는 입구

이 프로젝트가 흥미로운 이유는, 요즘 소프트웨어 업계에서 점점 중요해지는 '형식 검증'의 입문 통로가 되기 때문이에요. Lean이나 Rocq(구 Coq) 같은 '증명 보조기'라고 들어보셨나요? 컴퓨터가 수학 증명의 모든 단계를 기계적으로 검사해주는 도구인데요. 최근 수학계에서는 대형 정리를 Lean으로 검증하는 프로젝트가 활발하고, AWS는 핵심 인프라의 정확성을 형식 기법으로 검증하고, CompCert라는 C 컴파일러는 아예 통째로 증명된 채 배포돼요. 문제는 이런 도구들의 진입 장벽이 어마어마하게 높다는 거예요. 문법 배우다가 다들 나가떨어지거든요. Proof Machine은 그 세계의 핵심 아이디어, 그러니까 "증명은 신비로운 영감이 아니라 조립 가능한 구조물이다"라는 감각을 코드 한 줄 없이 체험하게 해줘요. Lean 커뮤니티의 'Natural Number Game'과 함께 형식 논리 입문용 양대 산맥으로 꼽을 만해요.

한국 개발자에게 주는 시사점

"나는 수학이랑 상관없는데?" 싶으시겠지만, 사실 여러분은 매일 증명을 하고 있어요. TypeScript의 타입 시스템이 바로 논리학이거든요. '커리-하워드 대응'이라는 유명한 이론이 있는데, 타입은 명제이고 프로그램은 그 명제의 증명이라는 내용이에요. 제네릭이 왜 그렇게 동작하는지, 유니온 타입과 인터섹션 타입이 왜 '또는'과 '그리고'처럼 움직이는지, 이런 게 전부 이 게임에서 배우는 추론 규칙과 같은 뿌리에서 나와요. 논리적 구조를 눈으로 직접 조립해본 경험은 복잡한 타입 퍼즐을 풀 때나, 코드 리뷰에서 "이 조건이면 이 케이스는 절대 발생 안 해요"라고 논증할 때 은근히 힘을 발휘해요. 주말에 커피 한 잔 들고 가볍게 몇 판 풀어보기 딱 좋은 분량이에요.

한줄 정리: 형식 논리 입문의 진입 장벽을 퍼즐 게임 수준으로 낮춘 수작. 여러분은 형식 검증이 앞으로 일반 소프트웨어 개발에도 확산될 거라고 보시나요, 아니면 항공·금융 같은 고신뢰 분야의 전유물로 남을까요?