[CobrastanJorji]

Yes, and his point is that finding that algorithm was, to Knuth, the interesting part. Getting from that to a proof was the boring bit.

[NewsaHackO]

Yeah, and I'm not sure what the other guy's argument is. It's Knuth, the primary researcher, who is giving the praise here. I don't see a possible motivation he would have to falsely give accolades to a AI for a problem he presented, then cleaned up to solve.

[OneManyNone]

That’s fair. Clearly Knuth himself thought it was impressive, that’s a strong signal.