No, but these tweets describe the basic concept: extension of AlphaZero to train on theorems in Lean automatically converted from natural-language proofs.
No, but these tweets describe the basic concept: extension of AlphaZero to train on theorems in Lean automatically converted from natural-language proofs.