If by solution you mean a proof and by testing you mean encoding it in lean and compiling it, the space of possible syntactically correct proofs which you can e

If by solution you mean a proof and by testing you mean encoding it in lean and compiling it, the space of possible syntactically correct proofs which you can encode probably explodes in a way that is well beyond what any computer could try to brute-force. LLMs don't brute-force proofs, i believe their approach is quite similar to humans. I believe the same is essentially true for counter-examples of the type that have been found latelly, they are not found by search, but by using theory. On the other hand even if the compute allocated by openai is esquivalent to day 10 human mathematicians, the machines can work 24h per day, that is already a lot more productive.