True the o1 model is the one exception though it's really more of a chain of LLMs. I wouldn't consider it a pure LLM.
Also, o1 still fails at many mathematical tasks which the linked article clarifies.
You don't see the majority of tokens it is generating.
Yes, I'm not claiming that is true formal reasoning, but it is certainly more of a chain of thought than was previously being done and does indicate that some questions require more and less "thought"