Yeah, but I wouldn't be surprised if they train the model on verification assisted by Lean