[amstan]

Are you sure the models did not have your exact solved proof already in their dataset?

[dash2]

No, it's very likely they did. But to have memorized one proof for every academic paper would be very demanding on parameters, I think.