Repository Issues

leanprover-community/mathlib4

The math library of Lean 4

View on GitHub
Stars
 (3,405 stars)
Forks
 (1,381 forks)
Indexed issues
 (16 indexed issues)
open beginner issues
 (0 open beginner issues)
Latest indexed
Jul 27, 2026
Last GitHub push
Jun 7, 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
No beginner labels indexed

Issues

16 open indexed issues

RSSAtom
Open
Tracking Issue: Digraph Targets
good first issuet-combinatorics

leanprover-community/mathlib4 #26,771 opened Jul 5, 2025 · Lean · 3,405 stars

Why recommendedHas a beginner-friendly label · Contributing guide available
Has a beginner-friendly labelContributing guide available
7 comments1 reaction2 assignees
Open
Sperner's lemma
good first issuet-analysist-combinatorics

leanprover-community/mathlib4 #25,231 opened May 27, 2025 · Lean · 3,405 stars

Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelContributing guide available
16 comments0 reactions0 assignees
Open
Tracking Issue: Naming consistency
good first issuehelp-wantedplease-adopt

leanprover-community/mathlib4 #21,584 opened Feb 8, 2025 · Lean · 3,405 stars

Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelContributing guide available
5 comments2 reactions0 assignees
Open
Define the Hodge star operator
enhancementgood first issuehelp-wantedt-algebra

leanprover-community/mathlib4 #17,722 opened Oct 14, 2024 · Lean · 3,405 stars

Why recommendedHas a beginner-friendly label · Contributing guide available
Has a beginner-friendly labelContributing guide available
2 comments3 reactions1 assignee
Open
The Shapley-Folkman lemma
good first issuet-analysis

leanprover-community/mathlib4 #14,427 opened Jul 4, 2024 · Lean · 3,405 stars

Why recommendedHas a beginner-friendly label · Contributing guide available
Has a beginner-friendly labelContributing guide available
8 comments1 reaction1 assignee
Open
Rename `rpow_le_rpow`
good first issueplease-adopt

leanprover-community/mathlib4 #13,544 opened Jun 5, 2024 · Lean · 3,405 stars

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

leanprover-community/mathlib4 #7,987 opened Oct 27, 2023 · Lean · 3,405 stars

Why recommendedNo assignee yet · Has a beginner-friendly label
No assignee yetHas a beginner-friendly labelContributing guide available
7 comments7 reactions0 assignees