Comment by clbrmbr

Can I start with a natural language description of the theorem to be proven and the model will automatically formalize it? And can I get a natural language interpretation of the Lean proof in case of success? --- I'm thinking of working through Elements of Abstract Algebra with this, but not sure if it has such general applicability?