Zulip Chat Archive

Stream: new members

Topic: Thank you


view this post on Zulip Jason Orendorff (Jun 20 2020 at 15:33):

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

view this post on Zulip Jason Orendorff (Jun 20 2020 at 15:34):

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

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 15:34):

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

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 15:34):

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

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 15:36):

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.

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 15:36):

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

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 15:37):

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

view this post on Zulip Jason Orendorff (Jun 20 2020 at 15:44):

It's exciting.

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 15:48):

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.

view this post on Zulip Ashvni Narayanan (Jun 20 2020 at 20:25):

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!


Last updated: May 14 2021 at 13:24 UTC