Thank you

Stream: new members

[Jason Orendorff]

Lean alternates between making me feel smart and making me feel incompetent and stupid.

[Jason Orendorff]

But this community is so helpful and kind. In case I've missed any of you: thanks

[Kevin Buzzard]

What happens as you go on is that Lean makes you feel smart more, and incompetent less.

[Kevin Buzzard]

And when you feel incompetent, it is sometimes the case that you've just discovered that something is set up wrong.

[Kevin Buzzard]

and then at some point you realise that the reason things are set up wrong is that actually humanity currently has quite a poor understanding of how to do undergraduate mathematics on a computer proof system, despite the fact that usable proof systems have existed for 30 years or more.

[Kevin Buzzard]

because most mathematicians don't use them, and most computer scientists don't have a good understanding of what mathematicians actually do.

[Kevin Buzzard]

so unfortunately we will remain occasionally feeling incompetent for a while yet, but it's going to get better, because times are changing.

[Jason Orendorff]

It's exciting.

[Kevin Buzzard]

It will inevitably change the world, but most mathematicians will not be interested until it actually starts changing the world. This creates a vicious circle, because it is not going to change the world until some time after mathematicians invest some time into teaching the system what mathematics is. And teaching systems mathematics e.g. by building mathlib is extremely unlikely to suddenly enable a tactic to prove a new theorem of interest to humans, at least in the short to medium term.

[Ashvni Narayanan]

Jason Orendorff said:

But this community is so helpful and kind. In case I've missed any of you: thanks

I second this. Thank you!