Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,915 Open 30,939 Closed
1,915 Open 30,939 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

chore: remove June 2025 deprecated declarations file-removed A Lean module was (re)moved without a `deprecated_module` annotation tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip WIP Work in progress
#33429 opened Dec 31, 2025 by Parcly-Taxel Loading…
1
doc(MeasureTheory): fix file refs t-measure-probability Measure theory / Probability theory
#33428 opened Dec 31, 2025 by harahu Loading…
1
ci: shorten bors timeout to 2 hours
#33427 opened Dec 31, 2025 by bryangingechen Loading…
1
chore: update Mathlib dependencies 2025-12-31 dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#33426 opened Dec 31, 2025 by mathlib4-update-dependencies-bot Loading…
1
feat: complex exponential is a covering map blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#33425 opened Dec 31, 2025 by urkud Loading…
3 tasks
2
ci: run check-lean4checker on self-hosted runner CI Modifies the continuous integration setup or other automation
#33424 opened Dec 31, 2025 by bryangingechen Loading…
1
feat: add an explicit trivialization for Complex.exp t-analysis Analysis (normed *, calculus)
#33423 opened Dec 31, 2025 by urkud Loading…
1
feat(Homotopy/Lifting): add a lemma about IsCoveringMapOn t-topology Topological spaces, uniform spaces, metric spaces, filters
#33422 opened Dec 31, 2025 by urkud Loading…
1
chore(Algebra/Order/Floor): review API about round, add continuity lemmas maintainer-merge A reviewer has approved the changed; awaiting maintainer approval.
#33421 opened Dec 31, 2025 by urkud Loading…
5
feat: OrderTypes 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-order Order theory
#33420 opened Dec 31, 2025 by YanYablonovskiy • Draft
74
feat: Have equality form for #t - #s in addition to the inequality new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-data Data (lists, quotients, numbers, etc)
#33419 opened Dec 31, 2025 by R-Peleg Loading…
2
refactor(RingTheory/Ideal/Basic): clean up proofs t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#33418 opened Dec 31, 2025 by tb65536 Loading…
1
feat: {Continuous}Linear{Isometry}Equiv.conj{Continuous, Star}AlgEquiv are "almost" injective blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
#33417 opened Dec 31, 2025 by themathqueen Loading…
1 task
3
chore(Order/GameAdd): add elab_as_elim attributes t-order Order theory
#33416 opened Dec 31, 2025 by vihdzp Loading…
1
chore(Analysis/SchwartzSpace): explicit variables for derivCLM and fderivCLM t-analysis Analysis (normed *, calculus)
#33415 opened Dec 30, 2025 by mcdoll Loading…
1
feat(Topology/Separation/NotNormal): generalize to non-separable spaces t-topology Topological spaces, uniform spaces, metric spaces, filters
#33414 opened Dec 30, 2025 by peakpoint Loading…
1
chore(CategoryTheory/Pi/Monoidal): monoidal Functor.pi and Functor.pi' t-category-theory Category theory
#33412 opened Dec 30, 2025 by robin-carlier Loading…
1
feat(Analysis/DiscreteConvolution): Discrete convolution API basics new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#33411 opened Dec 30, 2025 by IlPreteRosso Loading…
2
feat(LinearAlgebra/AffineSpace/Ceva): Ceva's theorem t-algebra Algebra (groups, rings, fields, etc)
#33409 opened Dec 30, 2025 by jsm28 Loading…
1
feat: add basics of majorization blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#33406 opened Dec 30, 2025 by dupuisf Loading…
1 task
2
chore(Algebra): move LinearMap.mul{Left, Right, LeftRight} to earlier file t-algebra Algebra (groups, rings, fields, etc)
#33405 opened Dec 30, 2025 by themathqueen Loading…
3
feat(Analysis/SchwartzSpace): scalar multiplication with linear factors t-analysis Analysis (normed *, calculus)
#33404 opened Dec 30, 2025 by mcdoll Loading…
1 task done
3
feat(GroupTheory/FiniteAbelian): prove that the restriction map is surjective
#33403 opened Dec 30, 2025 by xroblot Loading…
1
feat(LinearAlgebra/Transvection/Generation): prove exceptional case in Dieudonné's theorem blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-algebra Algebra (groups, rings, fields, etc)
#33402 opened Dec 30, 2025 by AntoineChambert-Loir Loading…
5 tasks
2
feat: IsStrictOrderedRing (Lex R⟦Γ⟧) delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory
#33398 opened Dec 30, 2025 by vihdzp Loading…
6
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.