倉庫議題

leanprover-community/mathlib4

The math library of Lean 4

在 GitHub 查看
星標
 (3,869 顆星)
分叉
 (1,592 個分叉)
已索引議題
 (17 個已索引議題)
個開放新手議題
 (17 個開放的新手議題)
最近索引
2026年8月10日
最近 GitHub push
2026年8月16日
授權條款
Apache License 2.0
貢獻指南
貢獻指南
行為準則
行為準則
主要語言
Lean
PR 合併指標
 (30 天內沒有已合併 PR)
新手標籤
good first issuehelp wanted

議題

17 個已索引議題

開放
Define a typeclass for GO-space
good first issuet-topology
為什麼推薦尚無負責人 · 帶有初學者友善標籤
尚無負責人帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #42275 · 2026年7月30日 · Lean · 3,869 顆星

1 則留言1 個反應0 位負責人
開放
The Gaussian as a Schwartz function
good first issuet-analysis
為什麼推薦尚無負責人 · 帶有初學者友善標籤
尚無負責人帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #33072 · 2025年12月19日 · Lean · 3,869 顆星

5 則留言0 個反應0 位負責人
開放
Define `Asymptotics.IsSubpolynomial`
good first issuet-analysis
為什麼推薦尚無負責人 · 帶有初學者友善標籤
尚無負責人帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #32658 · 2025年12月9日 · Lean · 3,869 顆星

3 則留言0 個反應0 位負責人
開放
Tracking Issue: Digraph Targets
good first issuet-combinatorics
為什麼推薦帶有初學者友善標籤 · 倉庫本月活躍
帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #26771 · 2025年7月5日 · Lean · 3,869 顆星

7 則留言1 個反應2 位負責人
開放
Sperner's lemma
good first issuet-analysist-combinatorics
為什麼推薦尚無負責人 · 帶有初學者友善標籤
尚無負責人帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #25231 · 2025年5月27日 · Lean · 3,869 顆星

16 則留言0 個反應0 位負責人
開放
Turn `compute_degree` into a simproc
good first issuet-meta
為什麼推薦尚無負責人 · 帶有初學者友善標籤
尚無負責人帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #22219 · 2025年2月23日 · Lean · 3,869 顆星

3 則留言1 個反應0 位負責人
開放
Tracking Issue: Naming consistency
good first issuehelp-wantedplease-adopt
為什麼推薦尚無負責人 · 帶有初學者友善標籤
尚無負責人帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #21584 · 2025年2月8日 · Lean · 3,869 顆星

5 則留言2 個反應0 位負責人
開放
Define the Hodge star operator
enhancementgood first issuehelp-wantedt-algebra
為什麼推薦帶有初學者友善標籤 · 倉庫本月活躍
帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #17722 · 2024年10月14日 · Lean · 3,869 顆星

2 則留言3 個反應1 位負責人
開放
The Shapley-Folkman lemma
good first issuet-analysis
為什麼推薦帶有初學者友善標籤 · 倉庫本月活躍
帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #14427 · 2024年7月4日 · Lean · 3,869 顆星

11 則留言2 個反應1 位負責人
開放
Rename `rpow_le_rpow`
good first issueplease-adopt
為什麼推薦尚無負責人 · 帶有初學者友善標籤
尚無負責人帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #13544 · 2024年6月5日 · Lean · 3,869 顆星

4 則留言0 個反應0 位負責人
開放
Small TODOs to do!
good first issue
為什麼推薦尚無負責人 · 帶有初學者友善標籤
尚無負責人帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #7987 · 2023年10月27日 · Lean · 3,869 顆星

7 則留言7 個反應0 位負責人
開放
Add typeclasses for smooth `(· • ·)`
good first issuet-differential-geometry
為什麼推薦尚無負責人 · 帶有初學者友善標籤
尚無負責人帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #5617 · 2023年6月30日 · Lean · 3,869 顆星

1 則留言0 個反應0 位負責人
開放
Extend basic API about `DomMulAct`
good first issue
為什麼推薦尚無負責人 · 帶有初學者友善標籤
尚無負責人帶有初學者友善標籤倉庫本月活躍提供貢獻指南

leanprover-community / mathlib4 · #5379 · 2023年6月22日 · Lean · 3,869 顆星

1 則留言0 個反應0 位負責人