Comment by ngruhn

8 hours ago

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.

0 comments