Search results

Add strategic game theory to Mathlib (Nash equilibria, stable matching, mechanism design)

Status: Open.

#41252 In leanprover-community/mathlib4;

· SMC17 opened on Jul 1, 2026

Rigidity Equality

Status: Open.

#40993 In leanprover-community/mathlib4;

· oukilwalid-prog opened on Jun 24, 2026

Header linter can repeatedly reparse Verso document bodies

Status: Open.

#40635 In leanprover-community/mathlib4;

· ejgallego opened on Jun 15, 2026

Morphism classes not used for integration and related issues

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open.

#40487 In leanprover-community/mathlib4;

· j-loreaux opened on Jun 10, 2026

Add global pull lemmas

t-linterLinterLinter

Status: Open.

#40183 In leanprover-community/mathlib4;

· grunweg opened on Jun 3, 2026

New tool for splitting up mathlib

Status: Open.

#40065 In leanprover-community/mathlib4;

· jmikedupont2 opened on May 31, 2026

Add PDecidable (like Decidable, but allows arbitrary sorts so it can hold data)

Status: Open.

#39751 In leanprover-community/mathlib4;

· srghma opened on May 23, 2026

Algebraic graph theory formalisation: Sabidussi, Lorimer, and the G₂(2) ecosystem

Status: Open.

#39717 In leanprover-community/mathlib4;

· RaggedR opened on May 22, 2026

Umbral calculus formalisation: finite operator calculus and Rota's classification

Status: Open.

#39712 In leanprover-community/mathlib4;

· RaggedR opened on May 22, 2026

Use Is*Apply classes

Status: Open.

#39639 In leanprover-community/mathlib4;

· mcdoll opened on May 21, 2026

SetRel: Examples don't show why α → β → Prop is worse than SetRel α β

Status: Open.

#39397 In leanprover-community/mathlib4;

· OrfeasLitos opened on May 14, 2026

Nonexistent SetRel.map in example

Status: Open.

#39396 In leanprover-community/mathlib4;

· OrfeasLitos opened on May 14, 2026