I wish there will be time when "(if correct)" would be nonsense because correctness is checked in a fraction of second by something like CoQ and this proof is accompanied every known theorem.