Repository Issues

leanprover-community/mathlib4

The math library of Lean 4

View on GitHub
Stars
 (3,869 stars)
Forks
 (1,592 forks)
Indexed issues
 (17 indexed issues)
open beginner issues
 (17 open beginner issues)
Latest indexed
Aug 10, 2026
Last GitHub push
Aug 16, 2026
License
Apache License 2.0
Contributing guide
Contributing guide
Code of conduct
Code of conduct
Dominant language
Lean
PR merge metrics
 (No merged PRs in 30d)
Beginner labels
good first issuehelp wanted

Issues

17 open indexed issues

Open
Define a typeclass for GO-space
good first issuet-topology
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #42275 · Jul 30, 2026 · Lean · 3,869 stars

1 comment1 reaction0 assignees
Open
Strict group homs are stable by `Prod.map`
enhancementgood first issuet-topology
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #38421 · Apr 23, 2026 · Lean · 3,869 stars

8 comments0 reactions0 assignees
Open
The Gaussian as a Schwartz function
good first issuet-analysis
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #33072 · Dec 19, 2025 · Lean · 3,869 stars

5 comments0 reactions0 assignees
Open
Define `Asymptotics.IsSubpolynomial`
good first issuet-analysis
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #32658 · Dec 9, 2025 · Lean · 3,869 stars

3 comments0 reactions0 assignees
Open
Tracking Issue: Digraph Targets
good first issuet-combinatorics
Why recommendedHas a beginner-friendly label · Repository active this month
Has a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #26771 · Jul 5, 2025 · Lean · 3,869 stars

7 comments1 reaction2 assignees
Open
Sperner's lemma
good first issuet-analysist-combinatorics
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #25231 · May 27, 2025 · Lean · 3,869 stars

16 comments0 reactions0 assignees
Open
Turn `compute_degree` into a simproc
good first issuet-meta
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #22219 · Feb 23, 2025 · Lean · 3,869 stars

3 comments1 reaction0 assignees
Open
Tracking Issue: Naming consistency
good first issuehelp-wantedplease-adopt
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #21584 · Feb 8, 2025 · Lean · 3,869 stars

5 comments2 reactions0 assignees
Open
Define the Hodge star operator
enhancementgood first issuehelp-wantedt-algebra
Why recommendedHas a beginner-friendly label · Repository active this month
Has a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #17722 · Oct 14, 2024 · Lean · 3,869 stars

2 comments3 reactions1 assignee
Open
The Shapley-Folkman lemma
good first issuet-analysis
Why recommendedHas a beginner-friendly label · Repository active this month
Has a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #14427 · Jul 4, 2024 · Lean · 3,869 stars

11 comments2 reactions1 assignee
Open
Rename `rpow_le_rpow`
good first issueplease-adopt
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #13544 · Jun 5, 2024 · Lean · 3,869 stars

4 comments0 reactions0 assignees
Open
Small TODOs to do!
good first issue
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #7987 · Oct 27, 2023 · Lean · 3,869 stars

7 comments7 reactions0 assignees
Open
Add typeclasses for smooth `(· • ·)`
good first issuet-differential-geometry
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #5617 · Jun 30, 2023 · Lean · 3,869 stars

1 comment0 reactions0 assignees
Open
Extend basic API about `DomMulAct`
good first issue
Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelRepository active this monthContributing guide available

leanprover-community / mathlib4 · #5379 · Jun 22, 2023 · Lean · 3,869 stars

1 comment0 reactions0 assignees