Issues

• Regular polygons

  help wanted
  SnirBroshi/mathlib4#124 · Filter by author SnirBroshi opened on Oct 2, 2026

• [Order/CompleteLatticeIntervals] transfer more lattice instances

  help wantedorder
  SnirBroshi/mathlib4#123 · Filter by author SnirBroshi opened on Sep 30, 2026

• [SimpleGraph] Triangle free lemmas

  graph-theoryhelp wanted
  SnirBroshi/mathlib4#122 · Filter by author SnirBroshi opened on Sep 26, 2026

• Ordinal-valued version of Order.height for WellFoundedLT

  SnirBroshi/mathlib4#121 · Filter by author SnirBroshi opened on Sep 20, 2026

• Linter for naming capitalization & underscores

  help wanted
  SnirBroshi/mathlib4#120 · Filter by author SnirBroshi opened on Sep 16, 2026

• [SimpleGraph] Bridgeless vs 2-connectivity, and common graphs

  graph-theoryhelp wanted
  SnirBroshi/mathlib4#119 · Filter by author SnirBroshi opened on Sep 15, 2026

• [Order] IsLowerSet/IsUpperSet predicates for arbitrary relations

  order
  SnirBroshi/mathlib4#118 · Filter by author SnirBroshi opened on Sep 9, 2026

• [Order] Every chain is finite iff well-founded in both directions

  order
  SnirBroshi/mathlib4#117 · Filter by author SnirBroshi opened on Sep 7, 2026

• Redefine [E]Nat.card

  SnirBroshi/mathlib4#116 · Filter by author SnirBroshi opened on Sep 7, 2026

• Use Function.IsConst everywhere

  help wanted
  SnirBroshi/mathlib4#115 · Filter by author SnirBroshi opened on Sep 7, 2026

• [SimpleGraph] Graham-Pollak theorem

  graph-theoryhelp wanted
  SnirBroshi/mathlib4#114 · Filter by author SnirBroshi opened on Sep 6, 2026

• [SimpleGraph] Kruskal's tree theorem

  graph-theory
  SnirBroshi/mathlib4#113 · Filter by author SnirBroshi opened on Sep 3, 2026

• [SimpleGraph] completeBipartiteGraph morphisms

  graph-theoryhelp wanted
  SnirBroshi/mathlib4#112 · Filter by author SnirBroshi opened on Sep 3, 2026

• [SimpleGraph/Bipartite] Generalize bipartiteDoubleCover

  graph-theoryhelp wanted
  SnirBroshi/mathlib4#111 · Filter by author SnirBroshi opened on Sep 3, 2026

• [Digraph/Orientation] Gallai-Hasse-Roy-Vitaver theorem

  graph-theoryhelp wanted
  SnirBroshi/mathlib4#110 · Filter by author SnirBroshi opened on Sep 1, 2026

• [SimpleGraph/LineGraph] Forbidden subgraphs characterization

  graph-theoryhelp wanted
  SnirBroshi/mathlib4#109 · Filter by author SnirBroshi opened on Aug 31, 2026

• [SimpleGraph/Cayley] Frucht's theorem

  algebragraph-theoryhelp wanted
  SnirBroshi/mathlib4#108 · Filter by author SnirBroshi opened on Aug 31, 2026

• [Order] Jordan-Dedekind chain condition

  help wantedorder
  SnirBroshi/mathlib4#107 · Filter by author SnirBroshi opened on Aug 30, 2026

• [LinearAlgebra/Matrix/Hermitian] Sylvester's criterion

  algebrahelp wanted
  SnirBroshi/mathlib4#106 · Filter by author SnirBroshi opened on Aug 29, 2026

• Renames: id/comp vs refl/trans

  help wanted
  SnirBroshi/mathlib4#105 · Filter by author SnirBroshi opened on Aug 29, 2026

• Rename diag to diagonal everywhere

  help wanted
  SnirBroshi/mathlib4#104 · Filter by author SnirBroshi opened on Aug 29, 2026

• [LinearAlgebra/Matrix/ToLin] Rename Matrix.toLin to Matrix.toLinearMap

  algebrahelp wanted
  SnirBroshi/mathlib4#103 · Filter by author SnirBroshi opened on Aug 29, 2026

• [Algebra/Polynomial/Roots] Polynomial.[a]root[Fin]set

  algebrahelp wanted
  SnirBroshi/mathlib4#102 · Filter by author SnirBroshi opened on Aug 29, 2026

• [GroupTheory] CA and CN groups

  group-theoryhelp wanted
  SnirBroshi/mathlib4#101 · Filter by author SnirBroshi opened on Aug 25, 2026

• Define Cardinal.choose and ENat.choose

  help wanted
  SnirBroshi/mathlib4#100 · Filter by author SnirBroshi opened on Aug 25, 2026