Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,975 Open 31,163 Closed
1,975 Open 31,163 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(LinearAlgebra/Projectivization/Action): prove that the action is 2-transitive and primitive large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#33715 opened Jan 7, 2026 by AntoineChambert-Loir Loading…
1
Riemannian metrics exist II new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-differential-geometry Manifolds etc
#33714 opened Jan 7, 2026 by idontgetoutmuch • Draft
1
ci: add commit verification for transient commits CI Modifies the continuous integration setup or other automation
#33713 opened Jan 7, 2026 by jcommelin Loading…
4
feat(Geometry/Euclidean/Angle/Unoriented/Projection):Add sameray_orthogonalProjection_vsub_of_angle_lt new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-euclidean-geometry Affine and axiomatic geometry
#33712 opened Jan 7, 2026 by wangying11123 Loading…
2
chore(AlgebraicGeometry/ProjectiveSpectrum): delete unused code ready-to-merge This PR has been sent to bors. t-algebraic-geometry Algebraic geometry t-meta Tactics, attributes or user commands
#33711 opened Jan 7, 2026 by Vierkantor Loading…
3
feat（Analysis/Convex/Between）:Add wbtw_of_sameRay_vsub_left new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#33709 opened Jan 7, 2026 by wangying11123 Loading…
2
chore: rename the commandStart linter to whitespace auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-linter Linter
#33708 opened Jan 7, 2026 by grunweg Loading…
6
ci: add commit verification for transient and automated commits CI Modifies the continuous integration setup or other automation
#33707 opened Jan 7, 2026 by jcommelin Loading…
1
chore: fix more spacing issues ready-to-merge This PR has been sent to bors.
#33706 opened Jan 7, 2026 by grunweg Loading…
5
feat: behavior under addition of the characteristic function of Value Distribution Theory t-analysis Analysis (normed *, calculus)
#33704 opened Jan 7, 2026 by kebekus Loading…
1
doc(Algebra/Quotient): update HasQuotient.Quotient doc-string delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc)
#33702 opened Jan 7, 2026 by JovanGerb Loading…
4
feat: dense orders have elements lying between two finite sets large-import Automatically added label for PRs with a significant increase in transitive imports t-order Order theory
#33700 opened Jan 7, 2026 by vihdzp Loading…
1
chore(Algebra/Ring): semireal definition lemmas t-algebra Algebra (groups, rings, fields, etc)
#33699 opened Jan 7, 2026 by artie2000 Loading…
2
feat(Algebra/Ring): characteristic of semireal ring t-algebra Algebra (groups, rings, fields, etc)
#33698 opened Jan 7, 2026 by artie2000 Loading…
4
feat(FieldTheory): real closed field t-algebra Algebra (groups, rings, fields, etc)
#33697 opened Jan 7, 2026 by artie2000 Loading…
13
fix(ci): show helpful message when runLinter needs master merge CI Modifies the continuous integration setup or other automation
#33696 opened Jan 7, 2026 by kim-em Loading…
6
feat(Mathlib/Analysis/Normed/Module): add instances of CompleteSpace for Submodules and ClosedSubmodule
#33693 opened Jan 7, 2026 by yoh-tanimoto Loading…
2
feat(LinearAlgebra/Transvection/SpecialLinearGroup): generation of the special linear group by transvections 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)
#33692 opened Jan 6, 2026 by AntoineChambert-Loir Loading…
8 tasks
2
feat(scripts): add find-ci-errors.sh to diagnose widespread CI failures CI Modifies the continuous integration setup or other automation delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).
#33691 opened Jan 6, 2026 by kim-em Loading…
5
feat: Defining Lie Rinehart algebras 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-algebra Algebra (groups, rings, fields, etc)
#33690 opened Jan 6, 2026 by Ljon4ik4 • Draft
16
refactor(Probability): make PMF return NNReal t-measure-probability Measure theory / Probability theory WIP Work in progress
#33689 opened Jan 6, 2026 by BoltonBailey • Draft
1
feat(PMF): add expectation lemmas for Poisson PMF new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory
#33688 opened Jan 6, 2026 by Citronhat Loading…
1
chore: tidy various files delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).
#33687 opened Jan 6, 2026 by Ruben-VandeVelde Loading…
@grunweg
8
fix(Tactic/DepRewrite): unknown free variable on rw! at local hypothesis t-meta Tactics, attributes or user commands
#33686 opened Jan 6, 2026 by plp127 Loading…
5
feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by an homotopy t-algebraic-topology Algebraic topology WIP Work in progress
#33683 opened Jan 6, 2026 by joelriou Loading…
1
ProTip! Type g i on any issue or pull request to go back to the issue listing page.