수학의 소프트웨어화: Lean과 증명 보조 도구가 묻는 시스템 설계의 본질

우리 모두 그런 경험이 있을 것이다. 거대한 Legacy 시스템을 리팩토링하면서, 이 변경사항이 시스템 어딘가에 숨어있는 엣지 케이스를 터뜨리지 않을까 전전긍긍했던 경험 말이다. 테스트 커버리지가 90%를 넘어도 불안감은 가시지 않는다. 완벽한 ‘증명’이 없기 때문이다.

최근 Quanta Magazine에 올라온 수학의 형식화(Formalization)와 Lean에 대한 기사를 읽으면서, 나는 수학자들이 현재 겪고 있는 진통이 우리 소프트웨어 엔지니어들이 수십 년간 겪어온 아키텍처 논쟁과 소름 돋도록 닮아있다는 것을 느꼈다.

Lean: 수학을 위한 CI/CD 파이프라인

수학에서 증명은 오랫동안 인간의 직관과 동료 평가에 의존해왔다. 하지만 현대 수학의 증명은 수백 페이지에 달할 정도로 복잡해졌고, 인간이 모든 논리적 비약을 검증하는 것은 불가능에 가까워졌다.

여기서 등장한 것이 Lean 같은 ITP(Interactive Theorem Prover)다. Lean은 본질적으로 수학을 위한 강력한 Type checker다. 수학적 정의와 정리를 코드로 작성하면, 컴파일러가 논리의 빈틈을 찾아낸다. 1+1=2라는 사실조차 공리로부터 완벽하게 도출되지 않으면 에러를 뱉는다.

Hacker News의 한 유저가 지적했듯, Lean의 가장 실용적인 기능 중 하나는 의도적인 공백을 허용하는 sorry 매크로다.

theorem fermat_last_theorem (n : ℕ) (hn : n > 2) :
  ¬ ∃ a b c : ℕ, a > 0 ∧ b > 0 ∧ c > 0 ∧ a^n + b^n = c^n := by
  sorry -- TODO: 이 부분은 나중에 증명함

이는 우리가 TDD를 할 때 껍데기 함수를 만들어두고 NotImplementedError를 던지게 하는 것과 완벽히 동일한 패턴이다. 전체 시스템의 인터페이스를 먼저 설계하고, 세부 구현은 나중에 채워넣는 Top-down 방식의 접근을 수학에 도입한 것이다.

과도한 추상화와 Bourbaki의 저주

기사에서는 1930년대 프랑스의 비밀 수학자 그룹 Bourbaki를 언급한다. 그들은 수학에서 구체적인 예시를 배제하고 극단적인 추상화와 엄밀함만을 추구했다.

솔직히 이 대목을 읽으면서, 비즈니스 로직은 뒷전이고 모든 것을 추상화된 Microservices와 인터페이스로 쪼개놓고 만족해하던 과거의 내 모습이 떠올라 뼈를 맞은 기분이었다. Bourbaki의 접근은 대수학이나 위상수학 같은 분야를 발전시켰지만, 시각적이고 직관적인 그래프 이론 같은 분야는 수십 년간 주류에서 밀려나게 만들었다.

시스템 아키텍처에서도 마찬가지다. 모든 것을 완벽하게 추상화하려는 시도는 필연적으로 특정 도메인의 발전을 저해한다. David Hilbert가 1905년에 남긴 명언은 소프트웨어 엔지니어링의 본질을 꿰뚫는다.

“과학의 전당은 기초를 먼저 단단히 다지고 나서 방을 짓고 넓히는 주택처럼 지어지지 않는다. 오히려 과학자들은 먼저 거닐기 편안한 공간을 찾고, 나중에 방을 확장할 때 기초가 부실하다는 징후가 나타나면 그때 가서 기초를 지지하고 강화해야 한다.”

MVP를 먼저 만들고, 트래픽이 몰려 병목이 생길 때 아키텍처를 개선하라는 현대의 Agile 철학이 100년 전 수학자의 입에서 나왔다는 사실이 놀랍지 않은가?

수학의 소프트웨어화: POSIX와 Leaky Abstraction

Hacker News 스레드에서 가장 흥미로웠던 논쟁은 고착화(Ossification)에 대한 부분이었다.

한 유저는 Lean 같은 시스템이 수학을 소프트웨어 개발처럼 만들며, 결국 특정 아이디어가 고착화될 것이라고 경고했다. 마치 운영체제 설계에서 더 나은 보안 모델이나 네임스페이스 구조를 만들 수 있음에도 불구하고, 하위 호환성 때문에 영원히 POSIX 레이어에 갇혀있는 것처럼 말이다.

하지만 이 비유에 대한 반론도 만만치 않았다. 소프트웨어의 추상화는 성능(Performance)이라는 현실적인 제약 때문에 필연적으로 Leaky Abstraction이 발생하지만, 수학의 추상화는 그렇지 않다는 것이다. 실수(Real numbers)가 어떤 공리계로 구축되었든, 한 번 증명된 속성은 하위 구현에 의존하지 않고 완벽히 동작한다.

물론 Constructive math나 선택 공리가 개입되면 이야기가 조금 복잡해지지만, 적어도 수학은 소프트웨어보다 훨씬 더 견고한 하위 호환성을 자랑한다. 우리가 NPM 패키지를 업데이트할 때마다 겪는 의존성 지옥이 수학계에는 덜하다는 뜻이다.

AI 시대의 수학: 기계가 증명하고 인간이 의미를 부여한다

결국 이 모든 흐름은 LLM과 맞닿아 있다. LLM은 새로운 수학적 진리를 발견하는 데는 젬병이다. 그들은 그저 가장 그럴듯한 패턴을 생성할 뿐이다. 하지만 LLM이 짠 그럴듯한 증명 코드를 Lean이라는 무자비한 Type checker가 검증한다면 어떨까?

이것은 우리가 GitHub Copilot으로 코드를 짜고 CI/CD 파이프라인의 테스트 코드로 검증하는 것과 정확히 일치하는 워크플로우다.

수학의 미래는 증명 그 자체에 있지 않을 것이다. 증명은 기계가 더 빠르고 완벽하게 해낼 것이다. 인간 수학자의 역할은 무한한 참의 명제들 속에서 ‘어떤 것이 인간에게 의미 있고 흥미로운 질문인가’를 찾아내는 도메인 전문가로 이동할 것이다.

결론 (Verdict)

수학계를 휩쓸고 있는 이 형식화의 물결은 단순한 유행이 아니다. 이는 학문적 엄밀함을 넘어, 인간의 인지적 한계를 시스템으로 극복하려는 거대한 엔지니어링 프로젝트다.

Lean이 모든 수학자를 대체하거나 모든 수학을 코드로 만들지는 않을 것이다. 하지만 복잡도가 임계점을 넘은 현대의 시스템에서, 기계가 검증할 수 없는 논리는 결국 레거시로 취급받게 될 것이다.

프로덕션 레벨의 소프트웨어를 다루는 엔지니어라면, 수학계가 겪고 있는 이 우아하고도 고통스러운 전환기를 유심히 지켜볼 필요가 있다. 우리가 매일 고민하는 시스템의 신뢰성과 추상화의 경계에 대한 가장 근본적인 해답이 그곳에 있을지도 모르기 때문이다.

References