Study note

Formalising Mathematics

View original Back to list

Properties

Type: Books
Status: 想读
Domain: Math
Category: 逻辑、集合论与范畴
Source: ma.imperial.ac.uk
Vault note: library/books/math/Formalising-Mathematics-64cb7316d9b0f47f.md

面向具有高年级本科数学经验的读者，结合 Imperial College 课程代码讲解如何用 Lean 4 和 Mathlib 形式化数学，并提供 Lean 实践技巧、常用 tactic 的说明与示例。

适合完成 Mathematics in Lean 基础章节后继续，把“会做教程题”推进到“能组织稍长证明、查 tactic 并阅读课程代码”。

Kevin Buzzard；2024。

Loading comments...