Comment by svat

No, the LLMs have been doing their reasoning in natural language, without Lean. Later, some of them were formalized from natural language into Lean, as a separate (also LLM-driven) effort. Only about half the papers in OpenAI's release were accompanied by Lean proofs, and this integer multiplication one wasn't one of them. (E.g. if you look at this https://lance.fortnow.com/openai-math-tcs.htm which is a subset of OpenAI's results, only some of the results have a Lean "badge".) The Lean formalization in the comment you responded to was done by others (as the comment says).