Yes that is the case. DeepMind's AlphaProof/Geometry that won IMO Silver used lean as an intrinsic part of the process 2 years ago, but things have shifted. When DeepMind and OpenAI won IMO Gold a year ago, it was solved end to end in language and translated to lean afterwards, and that has been the case since.