This is a deliberately bounded 3–5 day student project whose mathematical core has already compiled in isolation. The remaining work is careful packaging, one example, and integration into a serious long-term formalization program.
formalizationOn hold after campaign review
Package reduced-word inversion sequences as Finsets
For a reduced word in a Mathlib CoxeterSystem, add left and right Finset wrappers and prove the two cardinality and two inversion-membership lemmas requested in Langlands issue #47, plus a small finite example.
The issue identifies every Mathlib declaration needed and links a probe in which both definitions and all four core theorems already compile; reproduce that probe, integrate the module, and run repository diagnostics without `sorry`.
- Difficulty
- 2/10
- Attempts
- 0
- Last attempt
- Not yet
- Source status
- open
- External validation
- none
Lean 4Coxeter systemsList.toFinsetreduced-word inversions
Resumable campaign memory
0 epochs · 0 promising · 0 blocked · 0 ruled outResearch map
Select the cheapest new discriminator.
First action: Review the source and strategy registry.
Stop or redirect when: The planned discriminator resolves the route.
- No open lead is checkpointed.
- No strategy has completed an epoch yet.
- Nothing has been rigorously ruled out yet.
Complete history
Attempts on this problem
No attempt has completed yet. The problem is queued transparently.