[thomasahle]

> This is precisely how Google built AlphaProof! Read the article, Lean's role is quite critical to its success.

I read the article. It doesn't say anything about generating new proofs to train on. It only mentions scraping Github for lean theorems+proofs.

[Davidzheng]

I'm not sure if you're confusing alphaproof with leandojo here? Alphaproof generated its own proofs on 100M formal problems and did RL on this process.

[thomasahle]

Yes, I know AlphaProof did that. I wrote that it would be exciting "if they [LeanDojo] could integrate the reinforcement learning approach from AlphaProof".

This would give LeanDojo a lot more training data, and hopefully give us an open source proof assistant at IMO Silver level.

[Davidzheng]

Sorry!