PR !4#28962: chore: enable the flexible linter in mathlib

Stream: triage

[Random Issue Bot]

Today I chose PR #28962 for discussion!

chore: enable the flexible linter in mathlib
Created by @Michael Rothgang (@grunweg) on 2025-08-26
Labels: merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

[Michael Rothgang]

Still relevant (in my opinion). Needs a merge of master, dealing with the last instances in a good way --- and the biggest open question is if we have consensus for enabling it!

[Bhavik Mehta]

I'm very much in favour of enabling it, fwiw

[Michael Rothgang]

I know (and appreciate that). Convincing the other maintainers might be the biggest bottleneck here :-)