Maybe the reason the AI could find this proof is exactly what the author is complaining about: that it left the beaten path of theorems expected in a paper like this and went off in an unexpected direction.