Lean 4로 정리 증명하기

 Lean 4로 정리 증명하기🔗

Jeremy AvigadLeonardo de MouraSoonho KongSebastian Ullrich

with contributions from the Lean Community

이 문서는 Theorem Proving in Lean 4를 기계 번역 후 검토한 비공식 한국어 번역본입니다. 원문은 Apache License 2.0에 따라 배포되며, 이 문서에는 한국어 번역이라는 변경 사항이 적용되었습니다.

이 문서 버전은 Lean 4(구체적으로 4.33.0)를 사용한다고 가정합니다. Lean을 설치하려면 Lean 문서의 Quickstart section을 참고하십시오. 이 책의 첫 번째 버전은 Lean 2를 위해 작성되었으며, Lean 3 버전은 여기에서 확인할 수 있습니다.

Contents

  1. 1. 소개
  2. 2. 의존 타입 이론
  3. 3. 명제와 증명
  4. 4. 한정사와 동치
  5. 5. 택틱
  6. 6. Lean과 상호작용하기
  7. 7. 귀납적 타입
  8. 8. 귀납법과 재귀
  9. 9. 구조체와 레코드
  10. 10. 타입 클래스
  11. 11. 변환 택틱 모드
  12. 12. 공리와 계산