If I understand this correctly, they want to use an AI model for "autoformalization", which sounds like "using a language model to translate natural language pr

If I understand this correctly, they want to use an AI model for "autoformalization", which sounds like "using a language model to translate natural language proofs into Lean proofs". Which is cool but much less ambitious than the self-train system I described above. I guess AI technology isn't yet far enough to make such a proposal work.