1. That wasn't from Open AI or any major lab. I don't know what random people are getting to. It's curious also that it had no natural language proof attached. Usually these labs have a NL proof then translate to lean. Lot less possibility of lean maxxing.

2. None of the results Open AI retracted had an attached lean proof