Yes. The point was not coming up with the proof from scratch. The point was writing it all down in Lean to make it fully machine checkable.