Analysis I의 Lean 컴패니언

 (terrytao.wordpress.com)
2P by GN⁺ | ★ favorite | 댓글 1개
  • Terence Tao가 실해석 교재 Analysis I의 정의·정리·연습문제를 Lean 코드로 옮기는 컴패니언 저장소를 시작함
  • 자연수·정수·유리수·실수 구성과 집합론·논리를 엄밀하게 다루는 교재 특성상, 증명 보조기로 학습하기 좋은 구조를 가짐
  • 현재 범위는 2장 일부와 3.1 기본 집합론, 4.1 정수까지이며, Mathlib 자연수와의 동형도 포함됨
  • 코드는 Lean에서 컴파일되지만 많은 sorry가 남아 있고, 공식 해답 대신 포크에서 채워 넣는 방식을 권장함
  • 이 자료는 연습문제를 Lean으로 푸는 대체 경로이면서, 뒤로 갈수록 Mathlib 사용을 익히는 입문 자료로도 활용 가능함

Analysis I를 Lean으로 옮기는 프로젝트

  • Lean companion to “Analysis I”는 Analysis I의 여러 정의, 정리, 연습문제를 Lean으로 “번역”하는 프로젝트임
  • 책의 연습문제는 Lean 코드에서 대응하는 sorry를 채우는 방식으로도 풀 수 있음
  • 공식 연습문제 해답은 컴패니언에 호스팅하지 않을 계획이며, sorry를 채운 버전은 저장소 포크로 만들 수 있음

교재와 Lean이 잘 맞는 이유

  • Analysis I는 기존 실해석 교재를 보완하기 위해 기초적 이슈에 더 집중한 교재임
    • 자연수, 정수, 유리수, 실수의 구성
    • 높은 엄밀도의 증명을 개발할 수 있도록 하는 집합론과 논리
  • 책을 쓸 당시 Coq, Agda 같은 증명 보조기는 이미 있었지만, 형식 검증은 당시 관심사가 아니었음
  • 이후 형식 검증을 경험하면서, 책의 내용이 증명 보조기와 잘 맞는다는 점이 확인됨
  • 책에서 표준 수 체계를 구성할 때 암묵적으로 사용한 순진한 타입 이론은 Lean의 의존 타입 이론과 잘 맞음
  • Lean의 quotient type 지원도 책의 구성 방식과 맞물림

현재 Lean으로 옮겨진 범위

Mathlib과의 관계

  • 형식화는 일부 지점에서는 표준 Lean 수학 라이브러리 Mathlib와 분리되고, 다른 지점에서는 Mathlib에 의존하도록 설계됨
  • Mathlib에는 이미 표준 자연수 개념이 있음
  • Lean 형식화에서는 먼저 자연수를 “손으로” 다시 구성한 Chapter2.Nat를 개발함
    • Chapter2 네임스페이스에서 작업하면 Nat로 사용할 수 있음
    • Mathlib의 자연수 관련 보조정리와 평행한 기본 결과들을 설정함
    • 이 중 많은 증명은 독자 연습문제로 남아 있으며 현재 sorry로 대체됨
  • 에필로그 절에서는 이 대체 자연수와 Mathlib 자연수 사이의 동형을 세움
    • 더 정확히는 그 동형 역시 연습문제로 설정됨
  • 이후에는 2장의 자연수 구성을 더 이상 쓰지 않고, Mathlib 자연수를 사용함
  • 책의 뒤쪽 장으로 갈수록 앞 장의 자체 구성물보다 Mathlib 정의와 함수에 더 많이 의존하는 패턴을 이어갈 계획임

사용 방식과 검증 상태

  • 저장소 코드는 Lean에서 컴파일됨
  • 다만 코드 안의 많은 sorry가 실제로 모두 채워질 수 있는지는 아직 테스트되지 않음
  • 필요한 보조정리나 Lean 파일의 API가 충분한지도 확인이 필요함
    • 목표는 난해한 Lean 프로그래밍 기법에 의존하지 않고도 개념적으로 자연스럽게 sorry를 채울 수 있는지 확인하는 것임
  • 자원봉사자가 컴패니언을 플레이테스트해 실제로 연습문제를 Lean에서 풀 수 있는지 확인해 주기를 원함
  • 다른 피드백도 환영됨

Lean·Mathlib 입문 자료로서의 성격

  • 이 컴패니언은 실해석뿐 아니라 Lean과 Mathlib 입문에도 사용할 수 있음
  • 이런 성격은 Natural number game과 어느 정도 비슷함
  • Natural number game은 Analysis I의 2장과 주제적으로 겹치는 부분이 큼

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • 수학을 Lean으로 가르칠 때 가장 흥미로운 점은 즉각적인 피드백이라고 봄. 학생의 증명이 틀리면 그냥 컴파일되지 않음
    예전에는 조교, 강사, 전문가 같은 사람이 봐줘야만 피드백을 받을 수 있었지만, 이제는 Lean 컴파일러가 빠르게 피드백을 줄 수 있음
    앞으로는 Rust 컴파일러가 코드 수정 제안을 해주듯 Lean 컴파일러도 더 교육적인 피드백을 제공하면 좋겠고, 아마 전용 LLM이 필요할 수도 있음

    • 거의 전적으로 동의하지만, 증명 학습에서 느린 사고가 빠질 수 있다는 점은 고민됨
      예전 수학 공부는 과제를 두고 종이에 이것저것 시도하며 오래 곱씹는 시간이 많았고, 그 과정이 개념 내재화와 새로운 발상으로 이어지기도 했음
      Lean을 쓰면 막 시도하고 무작위로 확인하고 쏟아내는 방식이 될 수도 있지 않을까 싶음. Coq를 몇 번 만졌을 때도 주로 이것저것 만지작거리며 시도했던 기억이 남아 있음
    • Acorn은 이미 그런 식으로 동작함. 증명이 실패했지만 “거의 맞는” 경우 VS Code에서 다음 같은 제안을 보여줌
      reduce(r.num, r.denom) = reduce(a, b)
      cross_equals(a, b, r.num, r.denom)
      r.denom * a = r.num * b
      LLM은 쓰지 않고, VS Code 확장 안에서 작은 로컬 모델이 돌고 있음. 언젠가 그 작은 로컬 모델이 인간을 훨씬 뛰어넘을 정도로 강해지면 좋겠음. 자세한 내용은 https://acornprover.org/docs/tutorial/proving-a-theorem/에 있음

  • 정말 기대됨. 별도 저장소로 옮겨져서 찾고 다른 사람에게 보내기 쉬워지면 좋겠음
    원래 수학이 궁금했는데, Tao의 Analysis는 프로그래밍하는 머리가 기대하던 엄밀한 방식으로 수학이 어떻게 구성되는지 처음 보여준 교재였음
    이후 Lean도 조금 해봤고 비슷하게 만족스러웠지만, Mathlib은 수학 개념을 배우는 용도로는 꽤 복잡했음. 그래서 책과 도구를 잇는 다리가 생기는 게 반가움

    • 나도 수렴, 코시 수열 같은 내용을 그 책으로 배웠음. Hindustan Book Agency라는 지역 비영리 출판사에서 나와서 가격도 아주 저렴했음

  • 해석학 같은 주류 수학 주제에서 정리 증명이 탄력을 받는 모습을 보니 좋음
    프로그래밍 언어 이론 쪽에서는 이미 2010년대 중반 도구들이 꽤 다듬어지기 시작했을 때 Winskel의 The Formal Semantics of Programming Languages 같은 대표 교재가 Isabelle로 형식 검증된 적이 있음. 완전한 1:1 전사는 아니지만 http://concrete-semantics.org가 그 예임
    정리 증명에 관심이 있다면 개인적으로는 그쪽이 훨씬 쉬운 출발점이라고 봄. 해석학 정리들은 그 자체로 이미 꽤 어렵기 때문임

    • 프로그래밍 언어 증명이 입문용으로 더 쉬워도 놀랍지 않음. 사람들이 말하듯 훨씬 더 정형화된 절차가 많아 보임
      구조적 귀납법을 하고, 귀납 가정을 적용해 불변식이 유지됨을 보이고, 계속 진행하는 식임
      정리 증명을 많이 해본 것도 아니고 증명 보조기로 해석학 같은 “수학적” 증명을 해본 것도 아니지만, 수학 증명이 훨씬 다른 접근을 요구한다면 둘 사이에 기술 전이가 얼마나 되는지 궁금함
      Rocq의 Software Foundations도 언급하고 싶음. Lean 포트가 있을지도 모르지만, 초반부를 따라가 봤을 때 꽤 쾌적했음

  • 주류 “교과서”식 접근이 Mathlib의 접근과 어떻게 다른지 평가하는 일은 매우 흥미로울 것 같음
    일반적으로 형식화된 수학 라이브러리는 결과를 최대한 일반적으로 서술하고, 증명 전개를 더 직관적이고 우아하게 리팩터링하기 쉽게 만들어 줌
    리팩터링이 쉬운 이유는 시스템이 무엇이 무엇에서 논리적으로 따라오는지 항상 추적하기 때문임. 종이와 펜으로 작업할 때는 그게 없어서 재작업 기회를 놓치는 일이 많음
    학부 과정에서 Mathlib식 “최대 일반성” 버전의 실해석학을 가르치는 게 말이 되는지도 자연스러운 질문임. 물론 증명 기반 수학의 다른 분야도 마찬가지임

    • 입문 과정에서는 확실히 아니라고 봄. 이미 배울 게 너무 많음. 증명하는 법, 프로그래밍하는 법, 그리고 본래 과목 내용까지 있음
      실제로 시도해 본 교수진의 경험도 비슷한 것으로 알고 있음. 상급 학생에게는 괜찮지만, 평균적인 학생에게는 수업 시간을 낭비하게 될 가능성이 큼
    • 수학자이면서 오랫동안 프로그래밍도 해온 입장에서는, 어떤 프로그램식 형식주의도 기저 이해를 심어주는 데 실패할 것 같음
      내 편향은 수학 개념을 논문으로 배웠다는 데서 오긴 함
      코드는 추가 부담이 엄청나고, 대개 어떤 스타일 기준도 따르지 않는 경우가 많다고 느낌. 이해 불가능하다고 평가받는 수학 논문도 읽어야 했던 사람으로서 말하자면, 코드는 이해 가능성 기준이 사실상 거의 없어서 10배는 더 나쁨

  • Terence Tao 본인 YouTube 채널에도 Lean을 쓰는 영상이 몇 개 있음. https://www.youtube.com/@TerenceTao27
    자세히는 모르지만, LLM을 쓰거나 쓰지 않으며 작업하는 모습을 보는 게 멋졌음

  • 해석학처럼 기초적인 주제에는 아주 좋은 프로젝트이자 좋은 접근이라고 봄
    곧바로 떠오르는 걱정은 두 가지임. 첫째, Mathlib의 핵심 해석학 결과는 필터 개념을 사용해 극한을 일반적이고 통합적으로 다룸. 그래도 일부 결과는 엡실론-델타 형태로 특수화되어 있음. Tao의 Analysis는 더 전통적인 엡실론-델타 접근을 쓸 것으로 봄
    둘째, Mathlib은 빠르게 움직이고 자주 깨짐. 이름이 바뀌고 리팩터링이 계속 일어나서, 하위 저장소는 지속적인 유지보수가 필요함

  • 꽤 급진적인 생각이지만, 수학 교육은 Mathematica 같은 컴퓨터 대수 시스템과 Lean 같은 정리 증명기를 만드는 데 초점을 맞춰야 한다고 봄. 시각화와 실용적 응용도 강하게 포함해야 함
    극단적으로는 종이 수학을 전혀 하지 않으면서도 Lean 안에서 배운 모든 것을 증명할 수 있게 되는 형태일 수 있음
    지금 체계는 끝없는 수작업 계산에 집중하는데, 너무 쓸모없어 보이고 지루해서 사람들이 수학을 싫어하게 만든다고 느낌

  • Lean 교재라니 좋음. 그런데 왜 HoTT는 없을까?
    “Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?”
    https://news.ycombinator.com/item?id=43196452
    이번 주 HN에 올라온 추가 Lean 자료들:
    “100 theorems in Lean”
    https://news.ycombinator.com/item?id=44075061
    “Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean” https://news.ycombinator.com/item?id=44119725

    • HoTT의 여러 아이디어 형식화는 현재 Agda 커뮤니티에서 진행 중임. https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/
      정확한 동기는 내 분야 밖이라 모르지만, Agda가 Lean보다 그 아이디어들을 형식화하기에 더 나은 방식인 듯함
      올해 말에는 기존 HoTT 책의 더 현대적인 업데이트에 해당하는 새 교재도 나올 예정이고, Agda 형식화도 있음
      https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
      https://github.com/HoTT-Intro/Agda
    • HoTT는 매우 기술적이고 매우 좁은 주제라서, 이런 식으로 야심 찬 프로젝트 두 개를 동시에 다루는 건 말이 안 됨
      HoTT는 합리적인 표준으로 받아들여지는 데 전혀 가까이 있지 않고, 대부분의 사람에게는 시작부터 막히는 주제임
      JavaScript 프레임워크 개발자에게 왜 Elm이나 Haskell용 프레임워크를 만들지 않았냐고 묻는 것과 비슷함
    • 왜 HoTT가 있어야 하는지도 모르겠음
      HoTT 정리 증명기를 쓰기 편하게 만드는 데 투입된 작업이 훨씬 적고, 문서도 훨씬 빈약함
      HoTT의 이점도 불명확함. 범주론의 아주 난해한 구성물을 다룰 때만 작업을 줄여주는 것처럼 보임
    • “왜 HoTT가 없느냐”는 질문은 좀 이상함
      Terrence Tao에게는 해석학 교재가 몇 권 있고, 이것은 그 첫 번째 책에 대한 Lean 동반 자료임. 그는 유형 이론 교재를 갖고 있지 않으니 고차 유형 이론이 없는 것임. 애초에 하려는 일이 전혀 다름
    • 기존 교재에 대한 동반 자료라는 점만으로도 “왜 HoTT가 아니냐”에 답이 됨. 또 다른 이유로는 사람들이 그 교육적 가치를 의심하기 때문일 수도 있음

  • 아주 멋짐. Analysis I는 수학자가 아니라 엔지니어인 내가 Rudin 같은 다른 책들을 여러 번 시도한 뒤 처음으로 완전히 따라가며 풀 수 있다고 느낀 “진짜” 수학 교재였음
    Lean 동반 자료가 수학과 프로그래밍에 익숙하고 엄밀하게 배우고 싶은 사람들에게 더 접근하기 쉽게 만들어 주면 좋겠음

  • 지난 몇 년 동안 Tao의 Analysis I 책을 Lean으로 형식화하려는 시도가 꾸준히 있었고, 지금 Tao가 하는 것과 정확히 같은 일을 하려던 사람들이 있었음. 아쉽게도 대부분은 앞부분 몇 장을 넘지 못했는데, Tao는 더 멀리 갈 수 있기를 바람
    나도 직접 해볼까 생각했음. 내 Analysis I 해설 블로그 https://taoanalysis.wordpress.com/에 각 연습문제의 형식화된 증명을 붙이면 책을 따라가는 사람들에게 유용할 것 같았기 때문임
    책의 비공개 Discord 서버에도 올렸지만, 여기에도 도움이 될 만해 보여 관련 자료를 공유함
    https://github.com/cruhland/lean4-analysis — https://github.com/cruhland/lean4-axiomatic에서 가져옴
    https://github.com/Shaunticlair/tao-analysis-lean-practice
    https://github.com/vltanh/lean4-analysis-tao
    https://github.com/gabriel128/analysis_in_lean
    https://github.com/mk12/analysis-i
    https://github.com/melembroucarlitos/Tao_Analysis-LEAN
    https://github.com/leanprover-community/NNG4/ — Tao 책을 따르지는 않지만 Lean4 버전 자연수 게임이라 2장과 내용이 매우 비슷함
    https://github.com/djvelleman/STG4/ — Lean4 집합론 게임이라 3장과 비슷할 수 있음. 다만 https://github.com/djvelleman/STG4/blob/main/Game/Metadata.lean에 import Mathlib.Data.Set.Basic이 보여서 집합을 새로 정의하고 공리를 세우기보다 Lean의 집합을 가져오는 듯함. 이 접근은 Lean이 집합론에 대해 “너무 많이” 알게 만들어 목적에는 좋지 않을 수 있음
    https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc — 정수 구성용
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean — 위와 같은 파일일 수도 있음
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean — 유리수 구성용
    https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality — 사용자 정의 Set 타입을 정의하는 한 방법을 보여줌

답변달기