3 ms·
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.
by Davidzheng 2y ago
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 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!