It's not only Lean code, there are English writeups too. To my understanding the pipeline for these problems is 1) solve in english 2) formalize systematically to check. No one is tackling problems purely in Lean, to my understanding.

https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8...