1) You could train a different language model to translate between Lean and English. Use AlphaProof to do the hard work of theorem proving; use the translation model for interpretability and as a user interface. In fact, such a system could be ideal for formalizing a hundred years of English-language proofs.
2) This model is already specialized for math; applying it to other domains is out of scope. And as you point out, speaking Lean (and thus being verifiable) gives you an RL reward signal that's way more precise and readily available than piddly RLHF from human reviewers. Gyms like this are where AGI will happen.
(P.S. if anyone wants to work with me on reproducing AlphaProof, hit me up on Discord.)
Hi! I've been working on theorem proving systems for some time now. I would love to help out with an AlphaProof reproduction, but I can't reach you on discord for some reason!
2) This model is already specialized for math; applying it to other domains is out of scope. And as you point out, speaking Lean (and thus being verifiable) gives you an RL reward signal that's way more precise and readily available than piddly RLHF from human reviewers. Gyms like this are where AGI will happen.
(P.S. if anyone wants to work with me on reproducing AlphaProof, hit me up on Discord.)