So all this proves in #llm math problem solving are done with lean. So i guess if you know what to do a proof on and just randomly generating code until it fits is just bruteforce right? I guess thats the new intelligence they told us.