Zulip Chat Archive

Stream: new members

Topic: Thank you


Jason Orendorff (Jun 20 2020 at 15:33):

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

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

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.

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.

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.

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.

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.

Jason Orendorff (Jun 20 2020 at 15:44):

It's exciting.

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.

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: Dec 20 2023 at 11:08 UTC