▲

Analysis I의 Lean 컴패니언

 (terrytao.wordpress.com)
1P by GN⁺ 4일전 | ★ favorite | 댓글 1개
  • 테렌스 타오가 집필한 실해석학 교재 Analysis I의 핵심 내용을 Lean 증명 보조기로 옮긴 프로젝트임
  • 이 프로젝트는 기본 수 체계의 구성과 증명 논리 등, 엄밀성을 강조하는 원서의 목표와 잘 맞는 구조를 가짐
  • Mathlib 표준 라이브러리를 활용하되, 주요 개념을 직접 구축하고 독자들이 직접 증명하는 연습이 포함됨
  • Lean 코드상 빈칸(sorry) 을 직접 채우며 연습할 수 있어, 공식 해설은 제공하지 않고 포크(fork)로 확장 가능함
  • Lean 입문자 및 실해석학 학습자 모두에게 Mathlib과 Lean의 실제 활용법을 체험할 기회로 유용함

개요

  • 테렌스 타오가 쓴 실해석학 교재 "Analysis I"를 Lean 증명 보조기 도구로 재구성한 오픈소스 프로젝트임
  • 이 교재는 기존 다른 해석학 책들보다 자연수, 정수, 유리수, 실수의 구성 과정, 그 과정에서 필요한 집합론 및 논리적 도구에 더 초점을 맞춤
  • 책의 많은 부분이 체계적인 엄밀 증명 능력 개발에 초점을 두고 있어, Lean 같은 증명 보조기와 궁합이 잘 맞는 구조임

Lean 컴패니언 프로젝트의 특징

  • 원서의 정의, 정리, 연습문제를 Lean 형식으로 "번역"해 제공함
  • 이 Lean 파일들에는 연습문제 풀이에 해당하는 빈칸(sorry) 이 많이 포함되어 있으며, 이를 독자가 직접 채우는 방식으로 학습 가능함
  • 공식적인 해설(풀이)은 제공하지 않지만, 독자가 레포지토리를 포크해 자신의 해답 버전을 만들 수 있음

Mathlib와의 연계 및 차별성

  • Mathlib(Lean의 표준 수학 라이브러리)에 이미 구현된 개념(예: 자연수)은 일부러 별도로 직접 구축해보고, 이후 Mathlib 버전과의 동형성(등가성)을 증명해 보는 과정도 구성함
  • 예시로, Chapter2.Nat에서는 Mathlib의 자연수와 구분되는 자체 정의 natural numbers를 처음부터 구축하고, 주요 결과를 직접 다룬 후, 마지막에 두 버전이 동등함을 Lean에서 연습하도록 함
  • 이후 장부터는 Mathlib의 정의와 기능을 점점 더 많이 활용하는 흐름임

학습 및 활용 방법

  • 이 Lean 컴패니언은 해석학 학습뿐 아니라, Lean 및 Mathlib에서의 수학 공식화 방법에 대한 입문서 역할도 수행함
  • "Natural number game"처럼, Lean 환경에서 수학적 객체를 직접 정의·연습해 볼 수 있는 구조적 연습이 포함됨
  • 코드 자체는 Lean에서 컴파일이 가능하지만, 모든 연습문제(sorry)가 실제로 풀 수 있는지 완전 검증은 되지 않았으며, 이런 점에서 플레이테스트 및 피드백이 필요함

오픈소스 및 기여

  • 레포지토리는 오픈소스로 누구나 참고·포크·기여할 수 있음
  • 공식 솔루션은 따로 제공하지 않으며, 복수의 풀이 버전 생성을 지원함
  • 5월 31일 기준, 프로젝트는 별도 독립 레포지토리로 이전됨
▲
GN⁺ 4일전  [-]
Hacker News 의견

  • 나는 정말 기대가 되는 상황, 만약 이 프로젝트가 독립적인 레포로 옮겨지면 다른 사람들에게 쉽게 공유와 찾기가 더 쉬워질 것이라는 기대감, 나는 수학에 항상 궁금증이 있었고 Tao의 Analysis는 내 프로그래밍 사고방식에 맞게 엄격하게 수학이 어떻게 구성되는지 처음으로 보여준 교과서였다는 경험, 이후 Lean에도 빠져들었는데 Mathlib로 수학 개념을 배우기엔 조금 복잡함을 느낌, 그래서 책에서 툴로 이어지는 다리 역할을 해주는 이 프로젝트가 정말 마음에 든다는 이야기

    • 나도 비슷한 경험, 수렴, 코시 수열 등을 배웠고, 이 책이 인도 Hindustan Book Agency라는 비영리 출판사에서 출간되어 매우 저렴하게 구할 수 있었다는 추억 공유

  • 내가 Lean을 활용한 수학 교육에서 가장 신나는 부분은 즉각적인 피드백 제공이라는 점, 학생이 증명을 잘못하면 컴파일이 되지 않는다는 특징, 이전에는 TA나 교수 등 사람이 직접 피드백을 줘야 했지만, 이제는 Lean 컴파일러가 빠르게 알려줌, 앞으로 Rust 컴파일러처럼 더 친절하게 수정 제안까지 제공하는 기능이 생기길 바람 (이건 전용 LLM 도입이 필요할 수 있음)

    • 나도 거의 전체적으로 동의하지만, 증명을 고민하는 과정도 중요하다는 의견, 내 수학 경험은 오래전이지만 과제나 문제를 종이에 써가며 천천히 생각하는 '수학 낙원' 같은 시간이 많았음, Lean을 쓰면 오히려 무작위로 입력을 넣거나 자동으로 맞출 때까지 시도하는 '손놀림 위주'로 흐를 수 있다 걱정, 예전에 coq을 잠깐 써보기도 했는데 거의 계속 건드려 보기만 했었던 기억, 결론적으로 theorem solver가 많은 면에서 유용하지만 이런 천천히 곱씹는 과정이 사라지고 내재화, 개념화, 새로운 아이디어가 나오는 경로가 약해질 수도 있겠다는 고민, 이에 대한 생각이 궁금함

  • Terence Tao가 직접 Lean을 사용하는 영상을 볼 수 있는 개인 유튜브 채널이 있다는 이야기, 나는 이 분야 전문가는 아니지만 LLM을 함께 혹은 없이 작업하는 모습을 보는 것만으로도 정말 흥미로웠다는 관점 (https://www.youtube.com/@TerenceTao27)

  • 전통적인 "교과서식" 접근 방식을 Mathlib 방식과 비교 평가하는 것이 정말 흥미로울 것이라는 생각, 공식화된 수학 라이브러리는 일반적으로 최대한 일반적인 방식으로 결과를 표현하고, 증명 구조 자체를 리팩토링해서 우아하게 만들기가 쉽다는 장점, 리팩토링은 시스템이 논리적 종속성을 항상 추적해주기 때문에 손쉽게 할 수 있지만, 종이와 펜만으로 할 땐 쉽지 않음, 그래서 Mathlib처럼 '최대 일반성' 버전의 해석학을 대학 강의에서 가르치는 게 괜찮을지 자연스러운 고민이라고 봄, 이건 다른 모든 증명 기반 수학 분야도 마찬가지 고민이라는 의견

    • 적어도 입문 과정에서는 적합하지 않다는 입장, 이미 커리큘럼에 들어갈 것이 너무 많음 — 증명법, 프로그래밍법, 그리고 기초 이론까지, 실제로 시도해본 교수들의 경험도 비슷하며, 고급 학생에게는 좋지만 일반 학생에게는 시간 낭비라는 평가가 많다고 생각함

    • 나는 오랫동안 프로그래밍도 해온 수학자로서, 어떤 프로그램적 공식화도 근본적인 이해를 길러주지는 못할 거라고 생각, 내 편견은 내가 논문을 통해 개념을 배웠기 때문임, 코드가 종종 스타일을 신경 쓰지 않아 가독성 면에서 압도적인데, 비가독성 논문도 힘든데 코드의 경우 표준도 없어 10배 더 힘들다는 개인 경험

  • 정리 증명(theorem proving)이 해석학 같은 메인스트림 수학 분야에서 점점 주목 받는 게 반갑다는 소감, PLT에서는 이미 Winskel의 The Formal Semantics of Programming Languages라는 대표적인 책이 Isabelle로 공식 검증된 사례가 있었음 (http://concrete-semantics.org), 정리 증명을 시작해보고 싶다면 그쪽이 더 쉽고 추천할 만하다고 생각, 해석학에서의 정리는 원래 난이도가 상당히 높다는 점도 추가 설명

    • PL 증명이 더 진입 장벽이 낮을 것이라는 데에 나도 놀라지 않을 듯, 루틴화된 느낌이 많다는 이야기도 자주 들음 — 구조 유도(sturctural induction), 귀납법 적용, 불변식 증명, 반복, 이런 흐름, 나는 정리 증명을 많이 하진 않았지만 수학적(특히 해석학) 증명을 theorem prover로 해본 적은 없음, "수학적" 증명은 많이 다른 접근 방식을 요구하는지, 그리고 그 사이에 기술 이전(skill transfer)이 얼마만큼 될지 궁금, 참고로 Software Foundations in Rocq(Lean 포팅이 있을지도?)를 공부해봤는데 상당히 즐거웠다는 경험

  • 이 프로젝트와 접근 방식이 해석학 같은 기초적인 주제에 매우 잘 어울린다고 생각, 하지만 두 가지 걱정이 있음

    1. Mathlib의 해석학 핵심 결과는 필터(filter) 개념으로 통합적으로 다루는데, 특별한 경우에는 epsilon-delta형으로 별도 다룸, Tao의 Analysis는 좀 더 전통적 epsilon-delta 접근을 쓸 거라 예상
    2. Mathlib는 빠르게 변화하는 프로젝트라서 이름·구조가 항상 바뀜, 연동 정보는 지속적으로 관리해줘야 하는 문제

  • 매우 멋진 프로젝트라는 생각, Analysis I은 엔지니어인 내가 진짜로 처음으로 끝까지 다 따라가며 공부할 수 있었던 "진짜" 수학 교과서였고, 다른 책들(Rudin 등)에 여러 번 도전했다 실패한 경험도 있음, Lean 버전이 있으면 수학과 프로그래밍 둘 다 친숙한 사람들이 좀 더 엄격하게 개념을 배울 수 있게 될 것 같아 기대감

  • 수년간 Tao의 Analysis I 공식 Lean formalization 시도가 계속 있었지만 항상 몇 챕터 이상 진행되기 어려웠다는 사실, 한동안 나도 이 시도를 직접 하고 싶었음 — Analysis I 해답 블로그(https://taoanalysis.wordpress.com/)에 연계된 공식화 증명을 같이 올리면 책으로 공부하는 사람들이 유용하게 활용할 수 있을 거라 생각, 이미 비공개 Discord에 정리된 내용을 공유했지만 여기에 여러 사람들이 쓸만한 참고 Lean 프로젝트(github 및 gist, 공식 문서 등)들을 링크로 한 번에 공유함

  • "Mathlib에 해당하는 객체와의 동형(isomorphism) 증명"이 실제로 얼마나 중요할지 궁금, 혹시 동형 부분을 빼도 실질적으로 아무것도 변하지 않을 수도 있지 않을까, 예를 들어 정리를 자동 번역한다든가 그런 일에 실제로 쓰이나?

    • 이런 동형성(isomorphism) 증명은

      1. 자신이 만든 객체와 Mathlib에 이미 있는 객체가 실제로 동일함을 증명하게 해줌, 특히 Mathlib 쪽에서는 복잡하게 일반화된 구성으로 정의돼 있을 수 있어서 차이를 파악하는 데 도움이 됨
      2. Mathlib에서 그 객체를 읽거나 쓸 때 사용하는 공식적인 표기나 용어를 이해하는 데 결정적 역할

    • 최소한 교육적 가치가 있다고 생각, 내가 구성한 집합과 연산이 책 안에서 다른 곳에서도 '동일'하다는 것을 본인 스스로 납득하는 과정이 된다는 의미

  • Lean 기반 교과서 등장이 반가움, 그런데 왜 HoTT(Homotopy Type Theory)는 없을까? "Type Theory(HoTT)가 (ZFC) 집합론을 대체해야 하는가"라는 화두 기사도 존재 (https://news.ycombinator.com/item?id=43196452), 이번 주 HN에 올라온 Lean 관련 추가 커뮤니티 리소스도 함께 공유 — "100 theorems in Lean" (https://news.ycombinator.com/item?id=44075061), 그리고 DeepMind Lean 프로젝트 (https://news.ycombinator.com/item?id=44119725)

    • 그런데 굳이 HoTT까지 있어야 할 이유는 모르겠음, HoTT theorem prover는 아직 사용자 편의성이 낮고, 문서도 충분하지 않음, HoTT가 주는 이득도 명확하지 않다고 느끼는데, 보통 범주론 같은 극단적으로 특이한 구조 다룰 때만 유의미하다는 의견

    • 기존 교과서 방식이라서 "왜 HoTT가 아니냐"는 질문에는 이미 답변이 포함되어 있음, 게다가 교육적 효과에 대해 회의적인 전문가도 많다고 생각

답변달기