Search results

simps -fullyApplied should generate coe_ instead of _apply

t-metaTactics, attributes or user commandsTactics, attributes or user commands

Status: Open.

Feature

#37331 In leanprover-community/mathlib4;

· YaelDillies opened on Mar 29, 2026

flip vs Function.swap

Status: Open.

#36902 In leanprover-community/mathlib4;

· Komyyy opened on Mar 20, 2026

ClearExcept (clear * -) clears invisible auxiliary declarations (isAuxDecl) including recursive hypotheses

Status: Open.

#36722 In leanprover-community/mathlib4;

· oliver-butterley opened on Mar 16, 2026

Define dirac distribution

Status: Open.

#36464 In leanprover-community/mathlib4;

· aditya-ramabadran opened on Mar 11, 2026

False positives for tryAtEachStep linter and grind +suggestions tactic

Status: Open.

#36440 In leanprover-community/mathlib4;

· BartoszPiotrowski opened on Mar 10, 2026

Define strict maps between topological space

enhancementNew feature or requestNew feature or request

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

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

Status: Open.

#36269 In leanprover-community/mathlib4;

· ADedecker opened on Mar 6, 2026

Generalize Riesz' theorem to locally compact T2 topological vector spaces

enhancementNew feature or requestNew feature or request

good first issueGood for newcomersGood for newcomers

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

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

Status: Open.

#36134 In leanprover-community/mathlib4;

· ADedecker opened on Mar 4, 2026

feat(Algebra/Group): Add translator tactic for Subgroup and subgroupOf

Status: Open.

#35419 In leanprover-community/mathlib4;

· FrederickPu opened on Feb 16, 2026

feat(Computability): Step counting and complexity classes P/NP for TM1

Status: Open.

#35366 In leanprover-community/mathlib4;

· KrystianYCSilva opened on Feb 15, 2026

Tracking issue: extensions to the unused*In linter

Status: Open.

#35340 In leanprover-community/mathlib4;

· grunweg opened on Feb 15, 2026

Jordan Curve Theorem (JCT)

t-algebraic-topologyAlgebraic topologyAlgebraic topology

Status: Open.

#35222 In leanprover-community/mathlib4;

· SnirBroshi opened on Feb 13, 2026

Graph theory def: Maximal/maximum cliques & independent sets

help-wantedThe author needs attention to resolve issuesThe author needs attention to resolve issues

t-combinatoricsCombinatoricsCombinatorics

Status: Open.

#34962 In leanprover-community/mathlib4;

· SnirBroshi opened on Feb 7, 2026