Bumping mathlib to 3aae103 would break the build #277

mathlib incompatibility detected

An incompatibility has been detected between this project and recent changes in mathlib.
In other words, this project can't advance to the tip of mathlib without breaking.

First incompatible mathlib commit: 3aae103 — chore: replace irreducible_def with no_expose (#45063) (2026-10-28 (Jovan Gerbscheid)).

Last-known-good mathlib commit: 88126f7 — feat: import Counterexamples in the check-yaml script (#45378) (2026-10-27 (Lua Viana Reis))

Verified when LeanMachineLearning/LML was at: 61cd177 — Remove concentration duplication (#289) (2026-11-03 (Rémy Degenne)).
You can reproduce this break by:

• updating mathlib to 3aae103a67408fe3a11c1ac7950740a41a3cc5b1
• running lake update mathlib
• running lake build

downstream-reports reported at 2026-11-03T17:11:54Z · Workflow run · Job log · Failure log

This issue was last updated on 2026-11-03 by this workflow run. It is maintained automatically by downstream-reports/track-incompatibility. When the incompatibility is resolved, the issue is closed automatically with a comment.