The real answer in this case is that AlphaProof is a massively more complex training pipeline than the Qwen team’s pipeline. Sadly. Agreed that integrating Lean

The real answer in this case is that AlphaProof is a massively more complex training pipeline than the Qwen team’s pipeline. Sadly. Agreed that integrating Lean makes a ton of sense; it’s just probably an order of magnitude easier to do it inside DeepMind than elsewhere right now.