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?
1 comment
[ 2.3 ms ] story [ 12.1 ms ] thread