Study note

A Lean Companion to Analysis I

View original Back to list

Properties

Type: Blogs
Status: 待读
Domain: Math
Category: 代数几何、Lean 与可视化
Source: github.com
Vault note: library/articles/math/A-Lean-Companion-to-Analysis-I-fde7b6f91207bd94.md

把《Analysis I》中的自然数、整数、集合与实分析定义、定理和习题翻译为 Lean，代码中保留大量 `sorry` 供读者补全，并随着章节推进逐渐更多地复用 Mathlib。

提供“数学教材章节 -> 非形式证明 -> Lean 定义与定理 -> 补全证明”的真实项目闭环，适合基础入门后选择一节做小型形式化作品。

Terence Tao《Analysis I》的 Lean 4 伴侣项目。

Loading comments...