Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,384 Open 35,134 Closed
2,384 Open 35,134 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat(NumberTheory/Height): Heights of rationals (two lemmas) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38125 opened Apr 16, 2026 by rwst Collaborator Loading…
1
Deprecated decls with generic syntax linter test-ci A label used to help test CI actions
#38124 opened Apr 16, 2026 by adomani Contributor • Draft
1
chore: three more items for the overview documentation Improvements or additions to documentation
#38123 opened Apr 16, 2026 by grunweg Contributor Loading…
1
fix: properly tag structures with the stacks tag WIP Work in progress
#38122 opened Apr 16, 2026 by grunweg Contributor Loading…
1
chore(Data/Ordmap): put examples in a code block documentation Improvements or additions to documentation t-data Data (lists, quotients, numbers, etc)
#38121 opened Apr 16, 2026 by Vierkantor Contributor Loading…
1
refactor(Lie/Graded): remove a redundant assumption t-algebra Algebra (groups, rings, fields, etc)
#38120 opened Apr 16, 2026 by eric-wieser Member Loading…
1
feat(Topology/UniformSpace/DiscreteUniformity): finite discrete spaces are DiscreteUniformity t-topology Topological spaces, uniform spaces, metric spaces, filters
#38119 opened Apr 16, 2026 by NoahW314 Contributor Loading…
1
refactor: weaken assumptions in LpSeminorm/Count, ProductMeasure codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-measure-probability Measure theory / Probability theory
#38115 opened Apr 16, 2026 by yuanyi-350 Collaborator Loading…
6
feat(FinitelyPresentedGroup): add trivial instance new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-group-theory Group theory
#38114 opened Apr 16, 2026 by javgomzar Loading…
3
feat(SimpleGraph/PerfectGraph): add lemma graph is perfect iff all su… blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#38113 opened Apr 16, 2026 by robo7179 Loading…
2 tasks
3
perf: make sSup less reducible
#38111 opened Apr 16, 2026 by JovanGerb Contributor • Draft
4
feat(Topology): two theorems about extremally disconnected and irreducible t-topology Topological spaces, uniform spaces, metric spaces, filters
#38110 opened Apr 16, 2026 by felixpernegger Contributor Loading…
1
feat: add finitely presented instance for free groups awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-group-theory Group theory
#38109 opened Apr 16, 2026 by pacastega Loading…
@tb65536
13
refactor: golf only AEEqOfIntegral, AEMeasurableOrder, ConditionalExpectation/Real codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-measure-probability Measure theory / Probability theory
#38108 opened Apr 16, 2026 by yuanyi-350 Collaborator Loading…
4
refactor: golf only Function/SimpleFunc, Function/LpSeminorm/Basic, Constructions/Polish/Basic awaiting-author A reviewer has asked the author a question or requested changes. codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-measure-probability Measure theory / Probability theory
#38107 opened Apr 16, 2026 by yuanyi-350 Collaborator Loading…
12
feat(Topology/EMetricSpace): add Weak(Pseudo)EMetricSpace t-topology Topological spaces, uniform spaces, metric spaces, filters
#38105 opened Apr 16, 2026 by felixpernegger Contributor Loading…
1
refactor(MeasureTheory): golf 100 files blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-measure-probability Measure theory / Probability theory
#38104 opened Apr 16, 2026 by yuanyi-350 Collaborator Loading…
3 tasks
4
feat(Algebra/GroupWithZero/Action/Pointwise/Finset): add ₀ variants easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#38103 opened Apr 16, 2026 by b-mehta Contributor Loading…
1
feat(Order/Monotone/Basic): add Nat.stabilises_of_antitone t-order Order theory
#38102 opened Apr 16, 2026 by b-mehta Contributor Loading…
2
feat(Order/OrderIsoNat): add WellFoundedLT.antitone_chain_condition easy < 20s of review time. See the lifecycle page for guidelines. t-order Order theory
#38101 opened Apr 16, 2026 by b-mehta Contributor Loading…
1
refactor(Pointwise/Finset): use IsLeftRegular/IsRightRegular t-algebra Algebra (groups, rings, fields, etc)
#38100 opened Apr 16, 2026 by b-mehta Contributor Loading…
1
chore: make SMul.comp.smul implicit_reducible t-algebra Algebra (groups, rings, fields, etc)
#38098 opened Apr 16, 2026 by astrainfinita Collaborator Loading…
3
feat: add IndiscreteTopology instances t-topology Topological spaces, uniform spaces, metric spaces, filters
#38097 opened Apr 16, 2026 by NoahW314 Contributor Loading…
5
perf: try some funny class structure t-algebra Algebra (groups, rings, fields, etc)
#38096 opened Apr 16, 2026 by JovanGerb Contributor • Draft
2
perf(Algebra/*/{InjSurj, TransferInstance}): reduce instance Exprs t-algebra Algebra (groups, rings, fields, etc)
#38095 opened Apr 16, 2026 by astrainfinita Collaborator Loading…
7
ProTip! Mix and match filters to narrow down what you’re looking for.