CoT evidently helps but a bias towards both correctness and innovation has to come from somewhere. The article implies OpenAI's proofs may be supported by Lean but regardless, who knows how many people are trying to disprove the next conjecture each day throwing away nonanswers. Fundamentally these systems are more powerful with better training and sampling methods, or better prompting. Tokens matter but you can rewrite many prompts to get a much better, faster answer using fewer tokens vs allowing "thinking" to go on and on.