New Foundations의 일관성 – Lean으로 검증된 난해한 수학 증명

• 1937년 Quine이 제안한 집합론 New Foundations의 일관성 증명에서 어려운 부분이 Lean으로 검증됐고, 핵심 정리는 ConNF/Model/Result.lean에 정리돼 있음
• 접근 방식은 New Foundations와 Tangled Type Theory(TTT) 의 일관성이 동치라는 결과를 이용해, Lean 안에서 TTT 모델을 형식적으로 구성하는 것임
• TTT 모델은 낮은 타입 원소들로 집합이 유일하게 결정돼야 하는 외연성 때문에 구성 난도가 높아짐
• 모델 구성에는 기저 타입, t-set, 허용 가능한 순열, 작은 support, preferred extension이 쓰이며, 타입 크기를 μ로 제어하려면 freedom of action theorem이 필요함
• Lean 커널은 형식화된 증명을 검사하지만, 형식 문장이 의도한 영어 의미와 맞는지는 보장하지 않으므로 결과 해석에는 번역 검토가 필요함

---

Lean으로 완성한 New Foundations 일관성 검증

• 1937년 Quine은 집합론 New Foundations를 제안했고, Randall Holmes는 2010년부터 그 일관성 증명을 갖고 있다고 주장해 왔음
• 이 프로젝트는 Holmes 증명의 어려운 부분을 대화형 정리 증명기 Lean으로 검증해 New Foundations의 일관성을 보이는 데 초점을 둠
• 증명은 완료됐으며 정리 문장은 ConNF/Model/Result.lean에서 확인할 수 있음
  • source
  • docs
• 관련 자료도 함께 제공됨
  • Lean 코드 문서
  • deformalisation paper
  • blueprint

로컬에서 코드 실행하기

• 로컬 실행은 elan을 설치하고 저장소를 클론한 뒤, 저장소 루트에서 다음 명령을 실행하면 됨

lake exe cache get

• 이후 코드는 Visual Studio Code 같은 편집기에서 살펴볼 수 있고, 명령줄에서는 lake build로 직접 컴파일 가능함

New Foundations와 TTT의 연결

• New Foundations는 Tangled Type Theory(TTT) 가 일관적일 때 그리고 그때에만 일관적인 것으로 알려져 있음
  • 관련 결과는 Holmes의 theorem 1에 있음
• 프로젝트는 Lean에서 TTT 모델을 형식적으로 구성했고, 이를 통해 종이 위의 결론으로 New Foundations의 일관성, 즉 Con(NF) 를 얻음
• 작업은 Holmes의 여러 증명 문서를 바탕으로 진행됐지만, Lean의 타입 이론에 맞추기 위해 많은 변경과 추가가 필요했음
  • untangled.pdf
  • retangled.pdf
  • newnfdoc.pdf
  • maybedetangled.pdf

Lean 검증의 기반과 해석상 주의점

• 프로젝트는 Lean으로 작성된 커뮤니티 수학 라이브러리 mathlib에 의존함
• mathlib 덕분에 기수와 군 같은 익숙한 결과를 프로젝트 안에서 다시 증명하지 않고 사용할 수 있음
• mathlib와 이 프로젝트의 정의·정리는 Lean의 신뢰 커널이 검사함
  • Lean 커널은 구성된 증명이 실제로 올바른지 계산적으로 검증함
• 다만 Lean은 형식 문장이 의도된 영어 등가물과 일치하는지까지 확인하지는 못함
  • 코드에서 결론을 끌어낼 때는 영어 서술과 형식 문장 사이의 번역을 주의 깊게 봐야 함

Tangled Type Theory의 구조와 난점

• TTT는 등호 =와 포함 관계 ∈를 가진 다종류 집합론임
• 종류(sort)는 극한 순서수 λ로 색인되며, λ의 원소는 타입 지수라고 불림
• 식의 형성 조건은 타입에 의해 제한됨
  • x = y는 x와 y의 타입이 같을 때 잘 형성됨
  • x ∈ y는 x의 타입이 y의 타입보다 낮을 때 잘 형성됨
• 핵심 난점은 TTT의 외연성 공리에서 나옴
  • 타입 α의 집합은 임의의 타입 β < α 원소들로 유일하게 결정돼야 함
  • 예를 들어 타입 α의 두 집합이 다르면, 모든 β < α에 대해 서로 다른 타입 β 원소를 가져야 함
• 이 요구 조건 때문에 TTT 모델 구성은 단순한 집합론 모델 구성보다 까다로워짐

모델 구성의 주요 단계

• 기저 타입 구성

  • λ를 극한 순서수, κ > λ를 정칙 순서수, μ > κ를 공종도가 적어도 κ인 강한 극한 기수로 둠
  • 크기가 κ보다 작은 집합은 small이라고 부름
  • 모든 모델 타입 아래의 보조 타입인 레벨 -1의 base type을 먼저 구성함
  • 이 타입의 원소는 atoms라고 부르지만, ZFU나 NFU의 의미에서의 atom은 아님
  • atom은 μ개 있으며, 크기 κ의 litters로 분할됨

• t-set과 허용 가능한 순열

  • 각 타입 레벨 α에서 TTT 모델의 원소가 될 컬렉션을 만들며, 이를 t-set이라고 부름
  • 동시에 t-set에 작용하는 순열군인 allowable permutations를 구성함
  • 포함 관계는 allowable permutations의 작용 아래 보존됨
  • 각 t-set은 allowable permutations 작용에 대한 support를 갖도록 정해짐
  • support는 addresses라고 부르는 객체들의 작은 집합임
  • 어떤 allowable permutation이 support의 모든 원소를 고정하면 그 t-set도 고정함

• preferred extension으로 외연성 맞추기

  • 각 레벨 α의 t-set은 β < α인 어떤 타입의 preferred extension을 가짐
  • t-set의 원소들로부터 어떤 extension을 선호하는지 복원할 수 있고, 다른 낮은 타입의 extension은 그 β-extension에서 도출됨
  • 이 구조가 TTT의 외연성 공리를 만족시키는 데 사용됨

• 타입 크기 제어

  • 각 타입 α는 모든 β < α 타입의 크기가 정확히 μ라는 가정 등이 있어야 구성할 수 있음
  • 레벨 α의 t-set 컬렉션 크기가 적어도 μ임은 쉽게 증명되므로, 많아야 μ개라는 점을 보여야 함
  • 이를 위해 allowable permutations의 작용 아래에서 tangles의 근본적으로 다른 서술이 많지 않음을 보임
  • 이 단계에는 allowable permutations를 구성하게 해주는 기술적 보조정리인 freedom of action theorem이 필요함
  • 이 절의 주요 결과는 ConNF.mk_tSet에 있음

• 귀납 마무리와 공리 확인

  • 위 과정을 재귀적으로 실행해 모든 타입 레벨 α에서 tangles의 타입을 생성함
  • 집합론에서는 쉬운 단계지만, 필요한 여러 귀납 가정이 서로 얽혀 있어 타입 이론에서는 많은 작업이 필요함
  • 이후 구성물이 TTT의 모델인지 확인하기 위해 이론의 유한 공리화를 만족하는지 검사함
  • 프로젝트는 Hailperin의 NF comprehension scheme 유한 공리화를 TTT의 유한 공리화로 변환해 사용함
  • 결과 파일은 results file에 있음
  • 이 선택은 임의적이며, 이미 구축된 인프라를 사용하면 다른 유한 공리화도 쉽게 증명할 수 있음

[GN⁺]

Hacker News 의견들

• Lean으로 된 증명이 틀릴 위험은 매우 작다고 봄
  다만 Lean 버그와 무관하게, 소프트웨어 검증에서도 수학에서도 잘 알려진 위험이 있음: 결론을 정확히 읽어서 실제로 필요한 명제가 증명됐는지 확인해야 함
  Wilshaw의 최종 결론을 꼼꼼히 읽어봤고, 실제로 증명해야 할 것을 증명했다고 판단함

  • 논문도 비슷한 점을 말함: mathlib과 이 프로젝트의 모든 정의와 정리는 Lean의 신뢰 커널이 검사했고, 우리가 구성한 증명이 실제로 올바른지 계산적으로 검증함
    하지만 Lean은 정의와 정리의 명제가 의도한 영어 표현과 일치하는지는 확인할 수 없으므로, 이 프로젝트의 코드에서 결론을 끌어낼 때는 영어와의 번역을 조심해야 함

  • 내가 말한 문제는 라이브러리 관련 우려와 연결됨: 어떤 정의된 개념을 쓰면 그 정의가 올바른지, 즉 정말 필요한 것이 증명됐는지 확신해야 함
    Wilshaw의 형식화는 라이브러리를 쓰긴 했지만 이 반론에 취약하지 않음. 증명된 것은 어떤 정의된 개념이 1차 논리 공식들의 특정 묶음을 만족한다는 것이고, 그런 공식을 만족하는 술어가 있으면 NF는 일관적임

  • 또 다른 위험은 Lean 자체의 버그임. 정리 증명기에서 전례가 없는 일도 아님 1
    우연히 밟기는 어려울 수 있지만, 3처럼 임의의 사람들이 단계를 채워 넣는 대규모 협업이 점점 커지고 있음. 누군가 발견한 버그로 한 단계를 채워 넣어 방해하는 상황은 걱정할 만해질 수 있음

  • 기초론 관점에서는 이 증명이 NF와 Lean 커널 사이의 동등일관성에 대한 증명이라는 점도 중요함. Lean 커널 자체는 사람이 검토함
    기계화된 정리 증명기는 인간이나 다른 외부 시스템을 통해 주입된 올바름의 수준을 보존하는 방식임

• 내 착각이 아니라면, 이건 수년간 애매한 상태로 남아 있던 어려운 증명의 지위를 증명 보조기로 정리한 첫 사례로 보임
  Coq의 4색 정리처럼 신뢰되지 않는 소프트웨어가 큰 계산 요소를 맡은 기존 증명을 검증한 프로젝트는 있었지만, 더 넓은 수학 공동체에서 결과의 인식론적 지위 자체가 불확실했던 경우는 이번이 처음 같음

  • Liquid Tensor Experiment도 떠오름

    https://www.nature.com/articles/d41586-021-01627-2

    https://leanprover-community.github.io/blog/posts/lte-final/

  • 케플러 추측과 비슷한 상황임 (https://en.m.wikipedia.org/wiki/Kepler_conjecture)
    증명은 이미 알려져 있었지만, 형식화되기 전까지는 맞는지 확신하지 못했음

  • 다음은 abc 추측 차례일 듯
    2012년에 증명됐다고 주장됐고 400쪽 넘는 논문이 온라인에 있지만, 그 증명을 받아들이는 사람은 많지 않은 것 같음

• “New Foundations” 집합론 정식화가 다른 정식화와 비교해 무엇이 특별하거나 새로운지 대략 설명해줄 수 있나?
  아니면 수학 학부생이나 공학 전문가가 읽을 만한 설명 링크라도 좋음

  • 방금 Wikipedia 문서를 편집했는데, 이제 좀 더 읽기 쉬울 것임: https://en.wikipedia.org/wiki/New_Foundations
    핵심은 보편 집합의 존재라고 봄. 내 사용처인 프로그래밍 언어의 타입 시스템에서는 이런 보편 집합이 매우 유용함
    기존 시스템의 누적 우주나 type-in-type 같은 여러 우회책은 만족스럽지 않음. 대신 타입 시그니처가 층화되어 있는지만 확인한 뒤, 타입에 숫자 단계가 있다는 사실을 잊어버릴 수 있음
  • NF에서 미적으로 정말 마음에 드는 점은, “모든 집합의 집합”이 러셀의 역설을 일으키지 않도록 부분집합 선택 공리를 조정하는 방식임
    기본적으로 부분집합을 고르는 데 쓰는 술어가 아주 가벼운 타입 시스템을 지켜야 한다고 요구함. “x는 자기 자신의 원소가 아니다”는 합리적인 타입 시스템에서는 잘 타입화된 질문이 아니고, 특히 NF의 “층화 가능성” 요구도 만족하지 않으므로, 자기 자신을 포함하지 않는 모든 집합들의 집합이라는 러셀 역설의 집합을 만들 수 없음
  • NF의 “좋은” 점 하나는 공리/공리꼴이 두 개뿐이라는 것임: 1) 같은 원소를 가진 집합은 같다, 2) 임의의 층화 가능한 성질에는 그 성질을 가진 모든 것들의 집합이 대응한다
    “층화 가능”의 정의도 그리 복잡하지 않음. 반면 ZF에는 꽤 임시방편처럼 보이는 공리/공리꼴이 여덟 개 있음

• Coq와 Lean의 근본적인 차이가 무엇인지, 같은 종류의 논리 위에서 동작하는지 궁금해서 이 글을 찾았음 1
  그 논의는 거의 이해하지 못했고 둘 다 실제로 쓰지는 않음. 관련해서 더 설명할 내용이나 다른 증명 보조기와의 비교가 있으면 듣고 싶음

  1 https://proofassistants.stackexchange.com/questions/153/what...

  • 차이가 있고, 이 논의도 볼 만함 1

    1 https://github.com/coq/coq/issues/10871

• Lean 옹호자들이 표현을 조금 과하게 쓰는 것 같음. Lean은 종종 암시되는 것처럼 더 우월한 증명 방법이 아니라 대안적인 증명 방식임
  Lean을 배우려 들면 곧 알게 되는데, 자체 버그가 있는 프로그래밍 언어이자 시스템이고, 다른 인간들이 작성한 여러 라이브러리 스택에 크게 의존함. 그 라이브러리에는 선택이 들어가 있고, 빈틈이나 버그도 있을 수 있음
  그래서 “Lean이 그 증명이 좋다고 말했다”는 식의 표현에는 이견이 있음. 더 정확하고 정직한 표현은, 작성된 증명을 인간 수학자들이 검증했고, 그 증명을 인간이 Lean으로 번역해 거기서도 검증했다는 것이라고 봄. Lean이 유일한 황금 검증을 제공한다는 식은 꼭 정확하지 않거나, 적어도 그렇다는 설명을 보지 못했음. 부제인 “Randall Holmes 증명의 디지털화”가 가장 정확한 표현 같음

  • Lean 같은 강한 시스템에서 기계 검증된 증명은 인간만 검증한 증명보다 훨씬 우월하다고 봄. 인간은 놀랍지만, 지루해하고 세부사항을 놓치기도 함
    이건 단순한 이론적 주장이 아님. 사람들은 Euclid의 원론을 2천 년 넘게 읽고 나서야 빠진 공리를 알아차렸음. 제대로 작동하는 기계 증명 검증 시스템이라면 즉시 드러냈을 수준의 기본 실수임
    출판된 수학 증명도 나중에 틀린 것으로 밝혀지는 일이 많음. 수학이 점점 정교해지면서 인간이 모든 단계를 제대로 검증하기가 점점 어려워짐. 기계는 아직 증명 생성에는 인간만큼 좋지 않지만, 검증에는 견줄 데가 없음
    Lean과 “경쟁”하는 시스템들도 있으니 Lean이 “유일한 참된 길”이라고 하지는 않겠음. 예컨대 Metamath도 좋아함. 다만 이 시스템들 사이의 “경쟁”은 따옴표가 필요함. 각각 장단점이 다르고, 여러 시스템을 좋아하거나 쓰거나 기여하는 사람이 많음. 모두 인간에게는 비현실적인 엄밀도로 정리를 검증할 수 있음

  • 버그가 있을 수는 있지만, 신뢰해야 하는 것은 커널뿐이라고 이해하고 있음
    “다른 인간들이 작성한 여러 라이브러리 스택”이 mathlib을 뜻한다면, 그 말은 맞지 않는 것 같음. mathlib 코드도 결국 커널이 처리하는 코드로 컴파일되기 때문임
    웹사이트의 논문 초안 0도 이 점을 강화함: Lean은 큰 프로젝트지만, 받아들여진 증명이 올바른지 보장하려면 커널만 신뢰하면 됨. 전술이 잘못된 증명 항을 출력하더라도, 커널이 증명을 받아들이기 전에 그 실수를 발견할 기회를 가짐

  • 차이는 Lean에서는 커널만 신뢰하면 된다는 점임. 나머지는 그 위에 구성됨. 커널이 건전하면 다른 모든 것도 건전함
    이는 일반 프로그래밍 언어와 크게 다름. 일반 언어에서는 언제든 버그가 들어갈 수 있음. 또한 어떤 보조정리든 오류를 담을 수 있는 수학과도 크게 다름

  • 정리 증명기의 멋진 점은, 커널이 맞다는 전제하에 잘못된 증명은 컴파일조차 되지 않는다는 것임
    증명에 관해서는 전통적인 소프트웨어처럼 실행 시점에만 발생하는 버그가 없음. 실행 시점 자체가 없기 때문임
    Lean을 “일반” 프로그래밍 언어로 쓸 수도 있고 그때는 실행 시점 버그 위험이 있지만, 여기서는 그런 일이 아님

  • 정리 증명기를 오해하고 있음. 이건 “모든 추상화는 샌다” 수준의 얘기가 아님. 라이브러리를 신뢰할 필요가 없고, 커널만 신뢰하면 됨
    커널을 신뢰하는 것도 사소하지는 않지만, 비형식 증명에 비하면 큰 도약임. 비형식 증명에서는 실제로 “라이브러리”, 즉 문화와 다른 사람들의 지식을 신뢰해야 함. 공리까지 실제로 끓여 내려갈 실용적인 방법이 없기 때문임

• ZFC는 죽고 NF 만세인가?
  집합을 주로 다른 것을 설명하는 공통 언어로 쓰는 아마추어 수학자로서는, 이것이 더 넓은 수학 분야에 어떤 함의를 갖는지 잘 모르겠음. 특히 NF의 유용성이 기존 ZFC와 그 변형들과 비슷하다면 더 그렇음
  기계 증명에서 NF가 ZFC만큼 인기를 얻을 것으로 예상되나? 보편 집합의 존재는 더 직관적으로 느껴져서, 적어도 이 증명 덕분에 형식화에 대한 개인적 관심이 다시 살아남

  • 순진한 아마추어 관점에서는, 모든 ZFC 모형을 NF 모형으로 확장할 수 있으니 상대적 일관성 결과가 NF를 적어도 ZFC만큼 유용하게 만들어주는 것 같음
    하지만 다음 중 하나가 아니면 NF가 크게 유용해지지는 않을 듯함

    1. NF가 모순임을 증명한다. 그러면 ZFC도 모순임. 밤하늘의 별들이 하나씩 꺼지기 시작함 ;)

    2. ZFC가 모순임을 증명한다. 그러면 NF가 일관적일 가능성은 아직 남음. 행운을 빌어야 함

    물론 제대로 된 클래스에 대해 말할 수 있다거나, 층화된 공식으로 러셀의 역설을 피해 가는 등 NF의 더 실용적인 “삶의 질” 이점들을 놓치고 있을 가능성이 큼

  • NF를 독립적인 기초 체계로 밀려는 의도는 전혀 없음. NF는 꽤 특이한 체계임
    그래도 누군가 이를 밀고 싶다면, 이 일관성 결과는 적어도 ZFC에서 모순에 도달할 위험보다 더 크지 않다는 의미에서는 쓸 수 있다고 말해줌

• 이게 정말 마음에 듦
  결국 협업 증명과 “버그 수정”으로 이어져서, 수학이 GitHub의 코드와 비슷한 과정이 되지 않을까 궁금함

  • 이미 그렇게 되고 있음. Lean blueprint를 보면 됨: https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
  • 협업 증명이라는 아이디어는 꽤 오래전부터 있었고, 적어도 10년은 됐음: https://arxiv.org/abs/1404.6186

• mathlib 프로젝트를 따라갈 자유 시간이 있었으면 좋겠음. 정말 멋짐
  아주 느슨하게라도 참여할 방법이 있나?

  • Natural numbers game부터 시작할 수 있음

    https://adam.math.hhu.de/#/g/leanprover-community/NNG4

• 이 분야 사람은 아니지만, 충분히 강한 모든 체계는 자기 자신의 일관성을 보일 수 없다는 Gödel 정리가 있지 않았나?

  • 생각하는 건 Gödel의 불완전성 정리일 것임: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
    다만 체계 X가 자기 자신의 일관성은 증명할 수 없지만, 더 강한 체계 Y는 X의 일관성을 증명할 수 있음. 그리고 더 강한 다른 체계가 Y의 일관성을 증명할 수도 있음. 이렇게 각 체계가 더 약한 체계의 일관성을 증명하는 사슬이 생김
    이것이 그 체계가 절대적으로 일관적임을 증명하지는 않음. Y가 모순이면 X가 일관적이라는 것도, X가 모순이라는 것도 증명할 수 있기 때문임. 그래도 가치는 있음. 어쨌든 우리가 Y를 쓰는 이유 중 하나는 그 안에서 모순을 모른다는 점이기 때문임. 형식 체계는 종종 미묘하게 모순일 수 있으니, “다른 체계가 일관적이라는 가정하에 일관적”은 “일관성 증명이 전혀 없음”보다 훨씬 나음
  • 여기서는 그 체계가 자기 자신의 일관성을 증명하는 게 아님. 다른 더 강한 체계에서 일관성을 증명함
  • 흥미로운 점은, 설령 강한 체계가 자기 자신의 일관성을 증명할 수 있어도 그것만으로는 아무것도 알 수 없다는 것임
    모순인 체계도 자기 자신의 일관성을 증명할 수 있음. 따라서 어떤 체계가 스스로 일관적이라는 증명을 갖고 있어도, 실제로 일관적인지는 여전히 알 수 없음
  • 이 증명은 “Lean 4가 일관적이면 New Foundations도 일관적이다”라고 받아들이면 됨. Gödel의 불완전성 정리와 모순되지 않음
  • 여기서의 체계는 자기 기반 가정을 증명하려는 게 아니라, 기존 가정들의 집합 위에 쌓아 올리는 것 같음. 떠올리는 정리가 적용되지는 않을 듯함

• 만든 사람 중 한 명이 참여한 Reddit 논의도 볼 만함 0

  https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...