I have bounced off Lean a few times. What I wish I was able to achieve with it was to derive new and useful conclusions in mathematics. I can never seem to get past the "variable is an integer" examples. I realise that the objective in using these tools is exactly the problem in formulating your expression. I think it would be awesome if tools could generate novel mathematics. Where we could express "P=NP" and have computers just churn on that for a few thousand CPU hours.
What I wish I was able to achieve with it was to derive new and useful conclusions in mathematics.
That's a very high bar, and not likely to be reachable for quite some time. The most worthwhile, reasonably short-term goal in formalized mathematics is "simply" to completely formalize some sizeable part of the undergrad curriculum. (One should note that a proof formalization is publishable work on its own, because the process of formalizing a proof in some given system does help clarify the underlying working of it in a way that's not obvious from an informal sketch.)
Comments
I have bounced off Lean a few times. What I wish I was able to achieve with it was to derive new and useful conclusions in mathematics. I can never seem to get past the "variable is an integer" examples. I realise that the objective in using these tools is exactly the problem in formulating your expression. I think it would be awesome if tools could generate novel mathematics. Where we could express "P=NP" and have computers just churn on that for a few thousand CPU hours.
That's a very high bar, and not likely to be reachable for quite some time. The most worthwhile, reasonably short-term goal in formalized mathematics is "simply" to completely formalize some sizeable part of the undergrad curriculum. (One should note that a proof formalization is publishable work on its own, because the process of formalizing a proof in some given system does help clarify the underlying working of it in a way that's not obvious from an informal sketch.)