Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,449 Open 36,160 Closed
2,449 Open 36,160 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(fun_prop): allow fun_prop to call discharger on ModelWithCorners awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-meta Tactics, attributes or user commands
#39226 opened May 11, 2026 by lecopivo Collaborator Loading…
@grunweg
2
feat(SimpleGraph): add odd degree corollaries new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#39225 opened May 11, 2026 by junodeveloper Loading…
2
feat(Tactic/FunProp): allow discharging non-prop hypotheses awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-meta Tactics, attributes or user commands
#39224 opened May 11, 2026 by grunweg Contributor Loading…
1
feat(RingTheory/Extension): surjectivity and kernel of Cotangent.map t-ring-theory Ring theory
#39223 opened May 11, 2026 by BryceT233 Contributor Loading…
1
chore: centralise fun_prop tests
#39222 opened May 11, 2026 by grunweg Contributor Loading…
3
feat(NumberTheory/FLT): Beal conjecture bundle (4 files) 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-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#39221 opened May 11, 2026 by karlesmarin Loading…
4
feat(FieldTheory/Finite): add variant theorems for expand_card large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#39219 opened May 11, 2026 by WenrongZou Contributor Loading…
1
feat(Combinatorics/SimpleGraph/Walk): make p.Nil the simpNF of p = nil and p.length = 0 t-combinatorics Combinatorics
#39218 opened May 11, 2026 by SnirBroshi Collaborator Loading…
1
feat: locallyIntegrableOn_smul_iff awaiting-author A reviewer has asked the author a question or requested changes. t-measure-probability Measure theory / Probability theory
#39217 opened May 11, 2026 by grunweg Contributor Loading…
@ADedecker
10
feat(Topology\Algebra\InfiniteSum): add limUnder_eq_tprod new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-topology Topological spaces, uniform spaces, metric spaces, filters
#39216 opened May 11, 2026 by emlis42 Contributor Loading…
4
refactor(Data/Finsupp/MonomialOrder): remove .wf (well foundedness) field from MonomialOrder t-ring-theory Ring theory
#39214 opened May 11, 2026 by Hagb Collaborator Loading…
1
feat: define maximal cliques and independent sets LLM-generated PRs with substantial input from LLMs - review accordingly new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#39213 opened May 11, 2026 by m13683320924-hue Loading…
3
feat(Algebra\ContinuedFractions): add partNums! and partDens! new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)
#39212 opened May 11, 2026 by emlis42 Contributor Loading…
3
refactor: turn Set into a 1-field structure
#39211 opened May 11, 2026 by urkud Member • Draft
1
feat(Topology): test strictness on quotient and subspaces t-topology Topological spaces, uniform spaces, metric spaces, filters
#39210 opened May 11, 2026 by ADedecker Member • Draft
1
chore(Algebra/Polynomial): golf t-algebra Algebra (groups, rings, fields, etc)
#39208 opened May 11, 2026 by urkud Member Loading…
1
feat(Tactic/Linters/DeprecatedSimpLemma): lint for deprecated simp lemmas t-linter Linter WIP Work in progress
#39207 opened May 11, 2026 by Paul-Lez Collaborator Loading…
1
feat(Analysis/Calculus/AddTorsor/AffineMap): smoothness of AffineMap.lineMap t-measure-probability Measure theory / Probability theory
#39206 opened May 11, 2026 by FordUniver Collaborator Loading…
1
feat(Geometry/Convex): Bundled convex set large-import Automatically added label for PRs with a significant increase in transitive imports
#39205 opened May 11, 2026 by ooovi Collaborator • Draft
1
feat(Integral/CircleIntegral): add a convergence theorem t-measure-probability Measure theory / Probability theory
#39204 opened May 11, 2026 by urkud Member Loading…
1
refactor(Analysis/Calculus/Gradient): ungate inner_gradient lemmas t-analysis Analysis (normed *, calculus)
#39203 opened May 11, 2026 by FordUniver Collaborator Loading…
1
feat(Analysis/Calculus/Gradient): add toDual_gradient and companions
#39202 opened May 11, 2026 by FordUniver Collaborator Loading…
1
chore(SpecificGroups/Alternating/Simple): remove a convert t-group-theory Group theory
#39201 opened May 11, 2026 by b-mehta Contributor Loading…
7
feat(RingTheory/LocalRing/ResidueField/Fiber): the localization of Ideal.Fiber is a quotient t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#39196 opened May 11, 2026 by tb65536 Contributor Loading…
1
feat(Logic/Function/Defs): Add dcomp lemmas t-logic Logic (model theory, etc)
#39195 opened May 11, 2026 by linesthatinterlace Collaborator Loading…
3
ProTip! What’s not been updated in a month: updated:<2026-04-11.