This is explicitly labeled a good first issue, has a concrete proof architecture from a Mathlib maintainer, and is an unusually bounded formalization gap in topological-group infrastructure rather than a speculative open-ended theorem hunt.
formalizationOn hold after campaign review
Formalize that products of strict continuous group homomorphisms are strict
In Mathlib, prove that if f : G₁ →* H₁ and g : G₂ →* H₂ are continuous, topologically strict group homomorphisms, then Prod.map f g is strict; add the narrowly required API expressing strictness through rangeRestrict/kernel quotient and the existing IsOpenQuotientMap product theorem.
A Lean theorem with no axioms or sorrys, compiled by Mathlib CI; the issue identifies the existing lemmas IsOpenQuotientMap.prodMap and Homeomorph.Set.prod that provide an independently checkable proof route.
- Difficulty
- 4/10
- Attempts
- 0
- Last attempt
- Not yet
- Source status
- open
- External validation
- none
Lean 4 formalizationquotient-map characterization of strictnessproduct stability of open quotient maps
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.