使用Lean 4 的Mathlib 库的数学知识图谱

Lean 4 是一种计算机辅助证明系统(proofassistant)，或称交互式证明系统 (in teractive theorem prover)，可用于形式化验证数学定理或计算机程序的正确性。 Mathlib 是 Lean 4 的数学库，它背后有一个活跃的开发团队，包括许多数学家和计算机科学家。该系统已被应用于前沿的数学研究当中，例如，在数学Fields 奖得主Peter Scholze 发起的 liquid tensor 实验当中，人们成功地用 Lean 系统验证了condensed mathematics 中的一个关键定理。本项目基于 Lean 4 构建了知识图谱。

Өгөгдөл ба материал

图谱报告PDF _{【下载量：141】}
Шинжих
- Дэлгэрэнгүй мэдээлэл
- Татах
原始数据RAR _{【下载量：56】}
Шинжих
- Дэлгэрэнгүй мэдээлэл
- Татах
知识图谱TXT _{【下载量：75】}
Шинжих
- Урьдчилан харах
- Татах
LicenseTXT _{【下载量：9】}
Шинжих
- Урьдчилан харах
- Татах
实体 _{【下载量：44】}
Шинжих
- Дэлгэрэнгүй мэдээлэл
- Татах
关系 _{【下载量：33】}
Шинжих
- Дэлгэрэнгүй мэдээлэл
- Татах

Нэмэлт мэдээлэл

Талбар	Утга
Зохиогч	陈寅杰，葛郅琦，夏家桢
Арчлагч	葛郅琦
Сүүлийн шинэчлэл	хоёрдугаар сар 9, 2024, 05:43 (UTC)
Үүссэн	хоёрдугаар сар 9, 2024, 05:43 (UTC)