Walking through an example!
I wonder if eventually universities will start incorporating LEAN into their maths courses, e.g., introductory analysis courses. PS I think you have a typo in "resolves a goal if it the pattern of the statement an existing theorem"?
I wonder if eventually universities will start incorporating LEAN into their maths courses, e.g., introductory analysis courses. PS I think you have a typo in "resolves a goal if it the pattern of the statement an existing theorem"?