That sounds like the current proof is too brute-force—too badly understood by humans—for humans to be able to explain it to Lean?