To complexity theorists, this is an extremely funny situation; I bet OpenAI started by asking the bot about P vs NP and they got the worst-possible result, a useless and unexpected refutation of a conjecture. To be clear, I don’t trust Lean or OpenAI, so I don’t yet accept this result, but I hear Ryan Williams and Russell Impagliazzo are hand-checking the proof and I do trust them.