This is recognizable academic mathematics, but the bounded 2×2 computation reduces to matrix extensionality, finite cases, simp, and ring. It is an ideal easy-lane demonstration with a kernel-checkable result.
formalizationOn hold after campaign review
Formalize the standard 2×2 matrix sl₂ triple
Over a generic commutative ring, define the standard e, h, and f matrices, prove all three Lie-bracket relations, and prove nilpotence of e, f, and ad e, without attempting classification or Jacobson–Morozov theory.
The full representative theorem set already compiles in the linked Lean 4.28 probe; integration must pass diagnostics and contain no `sorry`.
- Difficulty
- 3/10
- Attempts
- 0
- Last attempt
- Not yet
- Source status
- open
- External validation
- none
Lean 4matrix Lie algebrasfinite extensionalitynilpotence
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.