Issues

• Duplicate lemmas in Pow/Real.lean

  leanprover-community/mathlib4#44800 · Filter by author keithadler opened on Oct 12, 2026

• Confirm introducing history for exists_injective_not_dense_image_deriv_ne_zero

  leanprover-community/mathlib4#44659 · Filter by author grwtsk opened on Oct 9, 2026
  1

• Generalize Hausdorff Measure

  leanprover-community/mathlib4#44658 · Filter by author CoolRmal opened on Oct 9, 2026

• Possible redundancy: Stream'.iterate and Nat.iterate

  leanprover-community/mathlib4#44510 · Filter by author lntricate1 opened on Oct 5, 2026
  1

• directoryDependency linter: new forbiddenDirs.json rules aren't checked against cached modules

  leanprover-community/mathlib4#44492 · Filter by author rosborn opened on Oct 4, 2026

• Generalize derivatives to LCTVS

  leanprover-community/mathlib4#44319 · Filter by author mcdoll opened on Sep 29, 2026

• Question/Issue with deriving Fintype for inductive types

  leanprover-community/mathlib4#44243 · Filter by author marcopist opened on Sep 27, 2026
  1

• move downstream_repos.yml to the community (or mathlib) website

  leanprover-community/mathlib4#44188 · Filter by author joneugster opened on Sep 25, 2026

• lake exe cache get not reporting decompressed files count after download finishes

  leanprover-community/mathlib4#44118 · Filter by author raoxiaojia opened on Sep 23, 2026

• Move away from unbundled relations in the Ordinal API

  leanprover-community/mathlib4#44009 · Filter by author vihdzp opened on Sep 20, 2026

• Add a Group instance for LieEquiv (automorphisms of a Lie algebra / Lie module)

  leanprover-community/mathlib4#43952 · Filter by author Yaohua-Leo opened on Sep 18, 2026

• Improve Multipliable.inv / inv₀ docstrings for ℂ (and add tprod_one_add_ne_zero_of_summable cross-reference

  leanprover-community/mathlib4#43872 · Filter by author s202101185-cell opened on Sep 16, 2026

• Subscript and superscript parsers should produce round-tripping Syntax

  leanprover-community/mathlib4#43870 · Filter by author mhuisi opened on Sep 16, 2026

• Notation for multilinear maps

  good first issue
  leanprover-community/mathlib4#43855 · Filter by author mcdoll opened on Sep 16, 2026

• Bare ⊢ ℝ unsolved goal when constructing IsPicardLindelof via of_time_independent with NNReal params

  leanprover-community/mathlib4#43614 · Filter by author snitgit opened on Sep 9, 2026

• Rename .lipschitz to .lipschitzWith

  leanprover-community/mathlib4#42869 · Filter by author TJHeeringa opened on Aug 17, 2026
  4

• @[to_dual] fails when a Decidable instance's argument is itself an ite

  leanprover-community/mathlib4#42852 · Filter by author kim-em opened on Aug 17, 2026
  2

• agda2lean

  leanprover-community/mathlib4#42793 · Filter by author chboishabba opened on Aug 15, 2026

• Missing: Sheppard's formula / Gaussian arcsine law E[sign X · sign Y] = (2/π) arcsin ρ

  leanprover-community/mathlib4#42600 · Filter by author overlordxrz-source opened on Aug 10, 2026

• docs: update docs with new material

  documentation
  Task

  leanprover-community/mathlib4#42593 · Filter by author luigi-massacci opened on Aug 9, 2026

• norm_num introduces Classical.choice on order goals over Nat/Int where decide does not

  leanprover-community/mathlib4#42565 · Filter by author zengineco opened on Aug 8, 2026
  1

• Define a typeclass for GO-space

  good first issuet-topology
  leanprover-community/mathlib4#42275 · Filter by author CoolRmal opened on Jul 30, 2026
  5

• calc? emits weird dagger characters

  leanprover-community/mathlib4#42155 · Filter by author FawadHa1der opened on Jul 27, 2026

• deriving CommRing on InfiniteAdeleRing generates opaque _aux_* field definitions that defeat isDefEq at instances transparency

  leanprover-community/mathlib4#42057 · Filter by author anagnorisis2peripeteia opened on Jul 24, 2026

• Ideas for contribution by undergraduate computer science students

  leanprover-community/mathlib4#42039 · Filter by author erelsgl opened on Jul 23, 2026
  1