3 ms·
> 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 ab
by thomasahle 2y ago
> 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 2y agoI'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 2y agoYes, 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.
- deleted 2y ago[deleted]
- Davidzheng 2y agoSorry!