tracking problem list: Group Theory, The Kourovka Notebook

A list of some specific **open problems** from [The Kourovka Notebook](https://arxiv.org/pdf/1401.0300)

- [x] 1.3 [Kaplansky.lean](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/Kaplansky.lean)
- [ ] 1.5 WIP
- [ ] 1.6
- [ ] 1.31
- [ ] 1.35
- [ ] 1.40
- [ ] 1.65
- [ ] 1.86
- [ ] 1.87
- [ ] 2.5
- [ ] 2.6
- [ ] 2.22
- [ ] 2.24
- [ ] 2.28
- [ ] 2.78
- [ ] 2.80 WIP
- [ ] 2.84 WIP
- [ ] 3.5
- [ ] 3.12
- [ ] 3.44
- [ ] 3.46
- [ ] 3.47
- [ ] 3.55
- [ ] 4.5
- [ ] 4.6
- [ ] 4.7
- [ ] 4.9
- [ ] 4.13 WIP
- [ ] 4.65 WIP
- [ ] 4.74
- [ ] 5.16
- [ ] 5.25
- [ ] 5.30
- [ ] 5.38
- [ ] 5.42
- [ ] 5.47 WIP
- [ ] 5.56
- [ ] 5.67
- [ ] 6.48
- [ ] 7.55
- [ ] 8.21
- [ ] 8.24
- [ ] 10.60 WIP
- [ ] 10.71
- [ ] 11.87
- [ ] 11.127
- [ ] 12.100 WIP
- [ ] 14.35 WIP
- [ ] 15.50

It seems that there the following definitions are not in the library: right-ordered group, pro-orderable group, nilgroup, abelian extensions, Engel group, locally soluble, locally nilpotent, locally finite, metabelian groups, ...
I don't know the mathlib well yet, tell me if they do exist.