Lean mathematical components library
active 2023-08-15 → 2024-07-21 (UTC)
Partial coverage20,506 / 26,262 hourly files (78%) · 2 absent upstream · 5,753 failed, retryable2023-08-15 → 2026-08-13 (UTC)— sampled evenly across the window, so rankings and trends hold; absolute counts scale up.
Events
584
Pushes
98
Pull requests
81
Issues
4
Stars
86
Forks
10
Activity over time
Daily event counts in the loaded window
Line chart, 342 days from 2023-08-15 to 2024-07-21. Pushes: 98 total, peak 18 in a day. Pull requests: 81 total, peak 11 in a day. Issues: 4 total, peak 1 in a day. Comments: 98 total, peak 13 in a day. Stars: 86 total, peak 5 in a day.
- Pushes
- Pull requests
- Issues
- Comments
- Stars
Top contributors
Pushes, PRs, issues, reviews and comments — stars and forks excluded, so this is contribution rather than popularity
| Contributor | Contributions | Pushes | PRs | Comments |
|---|---|---|---|---|
| YaelDillies | 103 | 20 | 37 | 43 |
| bors[bot] | 46 | 32 | 4 | 10 |
| eric-wieser | 30 | 9 | 10 | 10 |
| b-mehta | 18 | 17 | 0 | 0 |
| urkud | 17 | 1 | 3 | 9 |
| github-actions[bot] | 11 | 10 | 1 | 0 |
| mathlib-dependent-issues-bot | 7 | 0 | 0 | 7 |
| erdOne | 7 | 0 | 5 | 2 |
| adomani | 6 | 0 | 6 | 0 |
| BoltonBailey | 5 | 1 | 2 | 2 |
| jcommelin | 5 | 0 | 0 | 3 |
| alreadydone | 4 | 0 | 4 | 0 |
| leanprover-community-bot | 3 | 3 | 0 | 0 |
| mans0954 | 3 | 1 | 1 | 1 |
| linesthatinterlace | 2 | 0 | 1 | 1 |
| negiizhao | 2 | 0 | 1 | 1 |
| winstonyin | 2 | 0 | 2 | 0 |
| hrmacbeth | 2 | 0 | 1 | 1 |
| riccardobrasca | 2 | 0 | 0 | 1 |
| utensil | 2 | 0 | 0 | 1 |
Recent activity
Latest issues, pull requests and releases
- Issue comment#18135YaelDillies2024-07-04 21:18The Shapley-Folkman lemma
- Issue#18135YaelDillies2024-07-04 21:18The Shapley-Folkman lemma
- Issue comment#18135ndcroos2024-07-04 19:00The Shapley-Folkman lemma
- Pull request#19245alreadydone2024-06-28 02:36
- Pull request#19245alreadydone2024-06-28 02:36
- Pull request#19245alreadydone2024-06-28 00:09
- Pull request#19245alreadydone2024-06-28 00:09
- Issue comment#19225urkud2024-06-20 04:06refactor: change notation for interval integrals
- Pull request#19225urkud2024-06-20 04:06
- Issue comment#16502YaelDillies2024-06-09 07:19feat(data/rat/floor): add norm_num support for `int.{floor,ceil,fract}`
- Pull request#16502YaelDillies2024-06-09 07:19
- Pull request#18077YaelDillies2024-04-20 13:13
- Issue comment#16807semorrison2024-04-17 04:11feat(tactic/recommend): `recommend` tactic based on premise selection
- Issue comment#18158eric-wieser2024-03-23 23:18feat(algebra/order/ring/lemmas): use typeclass `zero_le_one_class`
- Pull request#18158eric-wieser2024-03-23 23:18
- Issue comment#16525eric-wieser2024-03-23 23:17chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace `without_zero_le_one`
- Pull request#16525eric-wieser2024-03-23 23:17
- Issue comment#16523eric-wieser2024-03-23 23:16chore(algebra/order/ring/lemmas): use suffix `ₚ`, create aliases
- Pull request#16523eric-wieser2024-03-23 23:16
- Issue comment#18405YaelDillies2024-03-23 21:41feat(topology/algebra/infinite_sum): Multiplicativise
- Pull request#18405YaelDillies2024-03-23 21:41
- Issue comment#17782YaelDillies2024-03-23 18:14chore(measure_theory/measure/haar_lebesgue): Golf
- Pull request#17782YaelDillies2024-03-23 18:14
- Issue comment#18257YaelDillies2024-03-23 17:40refactor(combinatorics/simple_graph/basic): Review `delete_edges` API
- Pull request#18257YaelDillies2024-03-23 17:40
Totals cover only the window loaded into ClickHouse and count events, not GitHub's lifetime totals — 86 stars here means stars gained during the window, not the repo's star count.