I don't understand anything. Are the contributions in Lean?

Did they start with OpenAI's Lean proof and continue work on that?

Does the Lean proof grow significantly, or are they also trying to keep the Lean proof short-ish?