수학은 유령이 있다

(overreacted.io)

2P by GN⁺ 2일전 | ★ favorite | 댓글 1개

Lean은 수학을 공식화할 수 있도록 설계된 프로그래밍 언어로, 수학자들이 수학 정리를 코드처럼 다루는 것을 가능하게 함
사용자는 정리, 증명, 공리 등을 코드 형태로 작성하며, 증명 과정은 tactic이라는 명령어 집합을 통해 진행함
증명이 실제로 완성되지 않아도 sorry로 임시 마감할 수 있으나, 이는 TypeScript의 any와 유사한 허위 증명임
공리를 잘못 추가할 경우(예: 2 = 3), 논리적 모순 및 모든 주장 증명 가능성이라는 위험이 발생함
Lean은 논리적으로 선택한 공리와 증명 체계 위에서만 결론을 산출하므로, 수학적 타당성 유지가 중요한 의미를 가짐

Lean: 수학을 코드로 다루는 언어

Lean은 공식화된 수학을 작성하는 데 특화된 프로그래밍 언어임
수학자들은 Lean을 통해 수학을 코드로 표현하고, 서로의 정리 및 증명을 구조화하여 협업 및 공유 가능함
앞으로 인류의 상당한 수학 지식이 코드 형태로 기계적 검증 및 조합 가능하게 되는 미래를 제시함

Lean 증명의 첫걸음

theorem two_eq_two : 2 = 2 := by sorry 형태로 Lean에서 간단한 정리 선언 가능
증명이 미완성일 때는 sorry를 넣지만, 이는 임시 방편일 뿐 실제 증명이 아님
- sorry는 Lean의 증명 검증을 통과시키지만, 논리적으로는 신뢰할 수 없음
완전한 증명을 위해서는 rfl(reflexivity)과 같은 tactic을 사용하여, 2 = 2처럼 자명한 등식을 증명함
이미 증명한 내용을 exact 등으로 다른 정리에서 재사용할 수 있어, 모듈성 강조

공리와 모순: 수학이 유령에 씌였을 때

만약 axiom math_is_haunted : 2 = 3과 같은 공리를 추가하면, Lean은 이를 참이라고 간주함
이 공리는 이후 증명 과정에서 활용 가능하며, 실제 수학적으로 말이 안 되는 결론(예: 2 + 2 = 6)마저 증명 가능해짐
rewrite tactic을 사용해 2를 3으로 치환, rfl로 등식 증명 절차를 마치는 것이 가능함
부적절한 공리로 인해 모순이 유도되면, Lean에서도 모든 명제 증명 가능 상태(논리적 붕괴) 발생
실제로 20세기 초 Russell의 패러독스 등 공리계 내 모순이 수학의 근본적인 고찰로 이어졌음
이렇듯 공리의 선택이 논리 체계의 타당성 유지에 결정적임을 Lean이 잘 보여줌

증명 검증기(proof checker)로서의 Lean

공리가 잘 선정되고 Lean이 논리적으로 올바르다면, 이론적 신뢰성 있는 결론을 제공함
간단한 등식부터 매우 복잡한 정리(예: Fermat’s Last Theorem)까지 모두 같은 원리로 검증함
대형 정리는 하위 구조와 정리의 반복적 증명 축적으로 전체 트리가 완성되는 구조임
예시로, Fermat's Last Theorem을 Lean에서 공식화하는 대규모 프로젝트가 진행 중이며, 최종에는 임시 증명(sorry) 없는 정식 증명 체계가 완성될 예정임

Lean을 배우는 즐거움

Lean을 통한 증명은 코딩과 수학의 창의적 결합임
처음엔 간단한 명제를 증명하는 법부터, 점차 복잡하고 깊은 수학을 엄밀하게 쌓는 과정이 중요한 즐거움이 됨
공식 자습서 및 커뮤니티 자료(예: Natural Numbers Game, Mathematics in Lean 등)가 입문에 적합함
Lean을 사용하면 직접 논리를 형식화하며, 교묘한 아이디어와 논증의 아름다움을 재발견할 수 있음
이유 없이도, 어떤 부류의 사람들에게는 Lean이 특별한 재미를 준다는 결론으로 마무리됨

▲

GN⁺ 2일전 [-]

Hacker News 의견

요즘 Lean과 비슷한 시스템(혹은 Lean 자체)을 이용해 뉴스나 논픽션 기사를 다시 써보는 아이디어를 생각 중임, 각 진술을 증명해야 할 정리로 보고 증명에는 인용도 포함시키는 방식임, 예를 들어 “내가 승인한 세 출처가 사실로 주장하면 이건 사실이다” 같은 합성 증명으로 처리할 수도 있음, 그리고 “증명된” 주장을 하이라이트해서 볼 수 있게 문서 전체를 마크업하는 게 가능할 것이라고 생각함, 완벽하진 않지만 요즘 언론이 담당하던 엄격함을 다시 한번 기술로 풀어보는 시도임
- 자연어 진술을 형식화하는 것은 수많은 난관이 존재하는 영역임, 실제 세계와 상호작용하는 코드를 작성하기 힘든 것과 비슷한 이유 때문임, 우리가 당연하게 여기는 개념들(동일성, 시간, 인과관계 등) 전부를 형식 속에서 세밀하게 다뤄야만 사실들끼리 연결되거나 표현 가능해짐, 그렇지만 이 문제는 정말 흥미로움, OpenCog가 이 분야를 끝까지 밀어붙인 프로젝트였고, 지식표현과 추론(KRR)이란 연구영역도 학계에 따로 존재함, IJCAI 저널도 이와 관련된 연구로 가득함, 그리고 철학자들이 시간/양상/확률 등 다양한 논증을 형식화하려고 쓴 논리들이 많은데, 안타깝게도 이들이 서로 쉽게 결합되지는 않음(아마 최근에 해결하지 않는 한)
- 뉴스에서 우리가 가져야 할 가장 중요한 신념은 대부분 절대적 진술의 모음으로 증명할 수 있는 것이 아니라고 생각함, 베이즈 확률과 같이 추론 연쇄를 계산하는 툴이 더 적합하다고 봄, 이런 식으로 수치적 추정을 위한 툴을 본 적 있음
- 수학을 대학에서 들은 후 논픽션 작문이 크게 향상됐다는 경험이 있음, 내 SO(애인)와 여동생이 쓴 에세이를 읽고, 마치 논리적 증명을 보듯 “여기서 C가 B로부터 나온다고 하는데 B가 A에서 나온 이유가 실은 빠져 있고, 그러면 C가 A에서 나온다고 할 수 없다” 같은 식으로 엄격함을 적용했었음, LLM 같은 도구로 이를 프로그램으로 만드는 게 가능해 보이긴 하지만, 환각 현상(사실에 없는 주장 생성)이 있어서 한계가 명확함
- 조심할 필요가 있음, 이런 접근이 논리적 객관성의 아우라를 본질적으로 아무리 급진적이거나 말이 안 되는 주장에 쉽게 부여해 줄 수 있음, 모던 로직의 아버지 중 한 명인 Gottlob Frege의 정치관을 보면 경고가 될 수도 있음 관련 링크
- 특정 주제에 대한 전체 논증 구조를 지도처럼 그리는 방법이 더 흥미로울 것 같음, 예를 들어 “신이 존재하는가?” 같은 큰 질문을 시작으로 찬반 논거, 그 반론, 그리고 반반론까지 전부 계층적으로 펼쳐 보는 것임, 각 주장마다 “플라톤이 이런 논증을 했다” 같은 식으로 인용은 근거라기보다 역사적 맥락 제공 용도로 넣는 것임, 승부를 가리는 게 아니라 동일한 논점에서 맴돌지 않도록 논증 지도를 만드는 것이 핵심임
우리가 결국 자명한 진리 몇 개로부터 출발하는 증명 사전을 만들어 그 위에 각종 증명이 논리적으로 쌓이는 구조를 만들고 있다는 건가 궁금함, 그럼 추가 증명은 그냥 이미 있는 증명들의 논리적 조합임, 이걸 Zachtronics 스타일 게임으로 만들어 줬으면 함! Euclidea라는 게임이 삼각법 분야에 이런 느낌을 주는데, 이렇게 논리의 탑을 쌓아가는 컨셉이 너무 매력적임, 순수수학이 바로 이런 건지 순수수학 교수들은 이 논리 사전을 확장하는 것에서 희열을 느끼는 건지 궁금함, 그리고 유명 수학자가 기본 증명 리스트를 만든 게 있었던 걸로 기억하는데 혹시 누구(무엇)이고 뭐라고 부르는지 알려주면 좋겠음, 아마 그것들이 공리(axioms)임
- 이미 관련 게임이 있는데 완전히 원하는 건 아닐 수도 있음 (그리고 수학 전체를 만드는 게임은 아님), 실제로 해봤는데 꽤 재밌었음, 이 기사에서 언급된 leanprover-community/nng4이 바로 그 예임
- “이걸 Zachtronics 스타일 게임으로 만들어 달라”에 답하자면, 수학이 바로 그 게임이라고 할 수 있음(약간 농담이지만), 게임 버전도 진짜 재밌을 거라고 생각함, 순수수학이 바로 그런 체계임, 학부 때는 그런 느낌이 맞고, 논문 연구로 올라가면 조금 다름, 게임 느낌을 원하면 Dummit and Foote 같은 추상대수 교재를 찾아보는 것도 추천함, 증명에 게임적 재미가 있음, 유명한 책들은 막히면 온라인에 해설도 있음
- 유클리드의 공리(axioms)를 말하는 걸 수도 있는데, 점, 선, 평면, 평행선 같은 개념이 정의된 체계임, 평면이 아니라 구 위에서는 이 체계는 깨짐, 혹은 Zermelo-Fraenkel 집합론(ZF/ZFC)을 언급하는 걸 수도 있는데, 현대 수학은 이 위에서 전부 구축됨
- Bombe라는 게임도 있는데, 마인스위퍼 변형임, 직접 셀을 여는 대신 “어떨 때 플래그를 놓을 수 있다”는 규칙을 만들면서 하는 게임임, 레벨이 높아질수록 래머(보조정리)처럼 규칙이 서로 연쇄됨, 플레이어 실력도 오르면 툴셋 제약을 풀어서 일반화도 가능해짐 게임 링크
- 수학은 본질적으로 공리에서 출발해 결론을 도출하는 과정임, 물론 그게 다는 아니겠지만 내 수준에서는 그렇게 이해하는 중임
약간 트집잡기는 하지만 two_eq_two 정리가 함수처럼 보인다고 하는 건 이상함, 인자가 없으니 오히려 상수에 더 가까움(물론 상수도 인자 없는 함수임은 알겠음), 아래처럼 x_eq_x를 써서 2_eq_2에서 함수처럼 적용하는 식이 더 설득력 있을 것 같음
```
theorem x_eq_x (x:nat) : x = x := by
  rfl

theorem 2_eq_2 : 2 = 2 := by
  exact (x_eq_x 2)
```
여기서 x_eq_x는 함수처럼 보이고, 2_eq_2에서 실제로 그런 식으로 쓰임
- 맞는 지적임! 내가 그렇게 안 한 건 Lean의 인자 처리(특히 dependent types 같은 콘셉트 — x를 주면 x = x 증명을 반환) 자체가 내겐 다소 생소하고, 따로 다뤄야 할 주제여서임, 다음 기사에서 다룰 예정임
Lean을 배우면서 느낀 어려움은 tactics(rfl 같은)들이 지나치게 포괄적이고, 튜토리얼로도 정확한 의미를 파악하기 어렵다는 점임, 예를 들어 C언어는 비트 단위까지 상태 변화를 추적할 수 있는데, Lean은 뭔가 불분명함, 그리고 rewrite(rw) 택틱 문법도 자연스럽지 않게 느껴짐
- Coq(이제 Rocq)에서도 tactics 적응이 항상 어려웠음, 예를 들어 “A = B”와 “P(A,A)”가 있을 때 “P(A,B)”로 옮기려 하는데, rewrite가 설명하기 힘든 이유로 먹히지 않았던 경험이 있음(중간 구조 정의의 문제일 것 같음), 반면 Metamath와 set.mm 데이터베이스는 아예 tactic 없이 구체적 추론만으로 증명하게 함(ax-mp 같은 추론 규칙만 사용), 근데 이건 이거대로 쓸 만한 유틸리티 레마를 다 외워야 해서 쉽지 않음
- 내가 Agda를 더 선호하는 이유 중 하나임, Agda는 사실상 tactic이 거의 없고, Curry-Howard correspondence를 이용해 함수형 프로그래밍 언어로 증명 term을 직접 씀, 대신 추상화와 함수 만들기를 게을리하면 사소한 것도 터무니없이 귀찮아지니 규율이 중요함
- 적어도 Lean에선 tactics 정의를 "정의로 이동(go to definition)" 해가며 내부 동작을 볼 수 있다는 점이 있음, 배울 땐 양이 많아서 버겁지만 결국 전부 살펴볼 수 있음(기초 타입 이론까지 가면 감이 잘 안 잡히지만), 그리고 rewrite 문법이 자연스럽지 않다고 했는데, 그렇다면 자연스러운 rewrite 구문이란 어떤 건지 궁금함
- 흥미로웠던 점은 tactics가 전부 "유저 레벨" 코드로, 증명 핵심(kernel) 바깥에 있다는 사실임, 작고 검증된 커널을 바꾸지 않고 유지하고 싶으니 이치에 맞음, 하지만 이 말은 tactics가 버전업이나 수정될 때 기존 증명이 깨질 수도 있다는 뜻임, 실제로 현실에서 그게 어느 정도 문제인지 궁금함
- 내 예상과 달리 Lean에선 reflection과 rewrite가 addition보다 더 근본적일 줄 알았음, Lean은 addition은 기본 제공하지만 rfl이나 rewrite를 매번 써줘야 하는 것 같음, 아마 Lean에는 prelude 같은 게 있어서 이걸 자동으로 해주는 버전이 있을지도 모르겠음
Lean에서 proof를 비대화식 noninteractive하게 읽는 방법이 있는지 궁금함, natural number game을 하다 보니 proof가 "rw [x]" 명령 나열로만 돼서 읽기 너무 힘들었음, 에디터로 각 줄 상태는 볼 수 있지만 계속 클릭해야 하니 흐름이 깨짐, 파이썬도 들여쓰기 없고 블록 구조만 보고 클릭해야 흐름을 파악해야 한다면 마찬가지일 것임, 내 관점은 게임 초반 제한된 명령어 때문일 수도 있는데, 실제 full Lean 환경에선 이 흐름이 더 괜찮은지 궁금함
- Lean에서 증명을 noninteractive하게 읽는 방법이 있나?
  나도 최근에 궁금해서 찾아봄, lean-in-latex 블로그가 클릭 없이 편집기 밖에서 그 흐름을 따라갈 수 있게 해주는 방법을 제공함, 그리고 Lean 커뮤니티가 이를 어떻게 접근하는지도 볼 수 있음
- Rocq에는 예전에는 “수학적 증명 언어”라는 게 있었음, 실제 사용 예시는 찾기 힘들지만 요런 느낌임
```
Lemma foo:
  forall b: bool, b = true -> (if b then 0 else 1) = 0.
proof.
  let b : bool.
  per cases on b.
    suppose it is true. thus thesis.
    suppose it is false. thus thesis.
  end cases.
end proof.
Qed.
```
  이런 접근은 논문에서의 “수기 증명”처럼 읽히게 만들었음, 근데 거의 안 써서 사라짐, Isabelle의 Isar proof 언어도 비슷하고, 오히려 표준 방식에 가까움, 예시:
```
lemma "map f xs = map f ys ==> length xs = length ys"
proof (induct ys arbitrary: xs)
  case Nil thus ?case by simp
next
  case (Cons y ys) note Asm = Cons
  show ?case
  proof (cases xs)
    case Nil
    hence False using Asm(2) by simp
    thus ?thesis ..
  next
    case (Cons x xs’)
    with Asm(2) have "map f xs’ = map f ys" by simp
    from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
  qed
qed
```
  전체 논리 구조와 중간 결과를 명확히 적어두고, 세부 디테일이 중요한 부분에서만 “by ...”로 tactic을 단축해서 쓸 수 있음, Lean에도 이런 게 있는지는 모르겠지만, 적어도 검색 키워드나 Lean 포럼 질문 소재로 참고가 될 수 있음
- 정말 좋은 질문임! 아직 초보라 완전히 신뢰하긴 어렵지만 내가 느끼는 걸 공유함, Lean을 두어 달 써본 결과, 증명 코드를 읽는 건 프로그래밍 코드를 읽는 것과 다르고, “스캔”하는 느낌에 가까움, 전반적 논증 구조, 어떤 tactic을 쓰는지, 어떤 lemma를 쓰는지에 주목하게 됨, 실제 Lean code 스타일은 새로운 goal마다 들여쓰기, goal 끝나면 다시 내어쓰기함, 그래서 argument의 모양(“shape”)이 중요하게 읽힘, 내 PR 예시 참고, tactic 익숙해지면 “intro”가 있으면 quantifier 진입임을, “constructor”는 goal 분할임을 등 알아챌 수 있게 됨, 결국 tactics는 증명 트리(term tree)를 만들어내는 매크로/DSL임, 나는 증명 코드를 볼 때 트리 조작(조각 나누기, 순서 채우기 등)처럼 느껴짐, 그래도 증명 코드 중간의 assertion을 정확히 알려면 클릭해야 하는 점은 여전히 남음, 좋은 아이디어를 가진 증명은 논문의 논리 전개처럼 명확하게 읽을 수 있음, 그래서 의도를 전달하려는 사람은 잘 읽히는 이름, 명확한 전개, 작은 lemma 추출, 그리고 가설을 먼저 적고 짧은 증명 코드로 해결하는 식으로 쓰게 됨, 반면 기계적으로는 번거롭지만 수학자 눈엔 분명한 부분은 “golfing”(최단 코딩)으로 처리함, 골프 스타일은 종종 코드가 짧아지는 대신 사람이 직관적으로 아는 부분만 다룸, 요약하면, Lean에서 읽는 구조는 암묵적이지만 더 명확히 할 수 있는 방법도 있고, tactic에 숙련될수록 클릭 없이도 구조를 더 잘 파악하게 됨, lemma 이름만 훑어도 큰 흐름을 알 수 있고, 순서는 쉽게 재구성 가능함
내용이 정말 좋았음, 이런 걸 쉽게 소화 가능한 방식으로 설명할 수 있는 사람이 드물다고 생각함, 전문가가 그냥 지나치는 작은 단계를 전부 보여주는 게 비법임
- 고마움!
혹시 이 스레드에서 Lean vs idris/coq/agda의 미래에 대한 의견을 들을 수 있을까 궁금함, 지식표현을 공부하려고 하는데 아무거나 파기 전에 커뮤니티 규모나 미래 리스크가 걱정됨, 예전엔 clojure core.logic에 시간 투자했다가 너무 저조한 관심/작은 커뮤니티 문제로 데인 적도 있어서 쉽게 시작을 못 하겠음
- 실제 경험으론 Lean과 Coq/Rocq가 Idris, Agda보다 훨씬 더 많이 쓰이고, 라이브러리·커뮤니티도 크다고 느낌, Rocq는 주로 프로그램 검증에 많이 쓰이는데, 그건 역사가 오래돼서 그런 거라고 생각하고 특이한 점도 많아서 Lean이 곧 따라잡을 수도 있음, Lean은 수학 정리 증명에 가장 흔히 쓰임, Rocq의 유명 프로젝트로는 CompCert, CertiCoq, sel4가 있고, 실제 항공기 소프트웨어 검증에 쓰는 사례도 있음(정리된 프로젝트 목록 참고), Lean에서는 mathlib(수학 증명 모음), 페르마의 마지막 정리(FLT 증명 프로젝트), PFR 등 대규모 프로젝트가 있음, Idris, Agda는 실제 “현실 세계” 프로젝트가 없다고 알고 있는데 혹시 틀릴 수도 있음, 모두 C++ 혹은 JavaScript 같은 언어나 커뮤니티에 비하면 규모는 매우 작음, 그리고 실제로 프로그램 검증은 매우 느리고 지루한 일임, AI 발전 등 근본적 변화가 언젠간 올 것 같긴 하지만 그래도 익힌 실력은 그대로 쓸 만함
- 이 분야에 베팅은 사실상 하지 않는 게 맞다고 생각함, 실제로 대부분의 수학자들이 formalization(형식화)에 큰 관심이 없음, 손으로 쓴 증명과 컴퓨터가 요구하는 엄격 구문 사이 간극이 크기 때문임, 그냥 배우고 실습하는 재미로 접근해야 하고, 미래 전망 면에서는 Lean이 최근 가장 활발한 편이긴 하지만 각자 오래된 사용자층이 있고, 예단은 어렵다고 봄
아무런 테크닉이나 변칙 없이도 그냥 Lean에 랜덤으로 어떤 걸 던지면 Lean이 통과(승인)하는지에 따라 흥미로운 발견이 나올 수 있는지 궁금함, 혹은 이런 걸 자동화 시스템이나 llm으로 돌려서 난해한 증명/이론을 모조리 시도해보고 성공여부를 보는 게 가능한지? 질문이 어색할 수 있지만 프로로그도 겨우 이해하는 수준임
- 내가 certfied programming을 직업적으로 하는 입장에서 보면, 생성형 AI와 포멀 메서드는 최고의 궁합이라고 생각함, 앞으로 프로그래머를 LLM이 대체할지 여부도 AI가 certified programming과 조합적 추론을 얼마나 잘 하느냐에 달렸다고 봄,
  
  랜덤으로 던지면 흥미로운 발견이 있나?
  기존 AI는 체커스 같이 경우의 수가 적은 문제에선 잘 됨, 체스는 조금 더 어렵고, 바둑은 머신러닝 없이 비전통 AI론 불가능할 정도임, 포멀 언어는 경우의 수, 탐색 가능한 상태의 수가 상상을 초월할 정도로 많음, 문제의 성질이 명확하면 SMT solver로 brute force가 가능함, 원래 SMT solver와 proof assistant는 다른 포멀 메서드 분과인데 이제는 서로 보완하는 세상이 됨(Sledgehammer, Lean-SMT 참조)
  llm이나 자동 시스템이 임의 증명/이론을 시도하게 한다면?
  이런 쪽은 아직 메인스트림 연구는 아니지만 연구가 많이 시도되고 있음, LLM 붐 이전부터 수년 간 대형 펀더가 있었음, “Learning to Find Proofs and Theorems by Learning to Refine Search Strategies” 같은 과거 시도, DeepSeek-Prover 같은 최근 연구도 있음, 아직 어떻게 학습시키고 미래 가능성이 어디까지인지는 완전히 열려 있음,
  현실의 LLM은 Rocq, Lean 언어에선 아직 미흡함, 그리고 잘못된 답이 나오면 고치기가 매우 고통스러움, 그래도 시간이 지나면 AI 도구의 수준도 크게 오를 거라고 기대함
- 이건 정말로 활발한 연구·실험 분야임!
  Lean 커뮤니티는 Zulip라는 곳에 많이 모여 있고, Machine-Learning-for-Theorem-Proving 채널에서 다양한 참고 스레드를 확인할 수 있음
alphaproof 보고 Lean에 처음 관심 가지게 된 입장에서 소개 글이 너무 좋았음, 혹시 Lean에서 뭘 하고 있는지 소개해 줄 수 있을까?
- 아직은 그냥 Lean으로 수학을 공부 중임, 구체적으로는 Tao의 Lean 교재를 따라가면서, 연습문제 중 비어있는 sorry 부분을 내가 채워 넣는 방식으로 공부 중임(내 해답들은 여기 있음)
Lean에는 불신뢰(proof with "sorry")가 쓰이거나 추가공리(axiom)가 계속 붙는 걸 자동으로 막을 수 있는 검증모드가 있는지 궁금함, 예를 들어 “proof가 어떤 방식으로도 sorry를 사용하지 않는다”, “고정된 공리 집합의 증명력에 의존한다”를 확인할 수 있나?
- 기사 후반에 언급된 #print axioms some_theorem이 해당 예시가 될 수 있지 않을까 싶음, 이걸로 그 증명이 직접 또는 간접적으로 sorry나 검토 안 된 공리에 의존하는지 알 수 있음
- print axioms로 추가된 공리가 없는지 확인할 수 있음, 그리고 warning이나 error 없이 컴파일되는지도 보면 됨, SafeVerify 유틸리티는 RL 시스템들이 찾아낸 몇몇 트릭도 잡아냄
- 매크로로도 이게 가능하다는 내용이 여기 있음

답변달기