Comment by ion_trapper

The proofs may not yet be understood, but to claim they should not yet be accepted as solved is to claim there is a bug in Lean, which is a big claim.