Will Lean be useful for me?

Stream: new members

[Ethan Kharitonov]

Im debating if I should spend time learning Lean but Im not sure if it will be usefull to me as a math undergrad. Can someone explain whether it will be usefull or not?

[Notification Bot]

A message was moved here from #new members > Hypotheses in branches by Johan Commelin.

[Johan Commelin]

@Ethan Kharitonov welcome! I moved your message to a new thread.

[Johan Commelin]

Whether Lean will be useful for you depends a lot on what you want to do with it

[Johan Commelin]

If your goal is to learn lots of maths in a short amount of time, then Lean will not be very useful, but I would rather encourage you to find a group of peers that are also ambitious to learn a lot of maths. Organise reading groups, go to undergrad seminars, etc...

[Johan Commelin]

If your goal is to learn how maths can be made 100% precise, and how computers can check proofs, or even search for proofs, then learning more about Lean will be a good investment.

[Kalle Kytölä]

I 100% agree with what Johan said.

But maybe an undertone in the question "if it will be useful to me as a math undergrad" is whether learning Lean as an undergrad will be useful after your undergrad studies. If that is a consideration, then I'd add that:

• Formalized math on the scale that we have today has a very short history --- no one really knows how useful Lean (and computer formalized math in general) will be even in the relatively near future (say 5 years), let alone during the whole future career of a current undergraduate student. Moreover the future usefulness is also not deterministic; it depends heavily on how many smart people (current undergraduates?) take it up and make most of it --- in both expected and unexpected ways. On this Zulip probably everyone believes that at least some aspects of formalization will be "useful" (whatever that means).

And in any case I think it is relevant to add the warning:

• Formalization is not just useful, it is also a lot of fun! The level of fun accessible with Lean & Mathlib may be dangerous during your undergraduate studies. But if one is able enjoy it in moderation, then formalization can have a positive impact on one's life.

[Kevin Buzzard]

Just do a project and stick it on github and then decide yourself whether it was useful.

[Bulhwi Cha]

Most math majors I met would say formalization is not useful for studying math, but I think Mathlib helps me understand math better. It's an actual implementation of math, so you can use it to find what was missing from your comprehension.

[Bulhwi Cha]

Besides, I make so many mistakes when writing by hand or in LaTeX that it's better to write Lean code. I just need a program that exports Lean math proofs into a format that mathematicians can understand who don't know anything about Lean.