Lean in daily maths

Stream: new members

[Jiatong Yang]

Can Lean replace our usual proofs on paper one day? (I think it has advantages as one can see clearly what has been done and what to do next, but now it takes a lot time thinking how to translate proofs to the lean language)
Are there teams working on Lean with AI?
(I don't know which topic it belongs to or whether it is proper to ask questions like this. I'm sorry for that.)

[Johan Commelin]

@Jiatong Yang See #Machine Learning for Theorem Proving for the "Lean with AI" question.

[Johan Commelin]

I would welcome a complete formalization of all known maths. But I think it will take several decades before that is a realistic goal.
Also, ITP's in their current form cannot replace doodling on a piece of paper, which is a very important proof technique. So they should add to our existing toolkit, but they certainly aren't ready to replace the existing methods (if the even ever should!!)

[Mario Carneiro]

there are computer replacements for doodling on a piece of paper, although I think you need a good tablet setup to use one

[Johan Commelin]

Sure, but afaik none of those is connected to an ITP

[Mario Carneiro]

I will be very impressed if a program manages to interpret my shitty drawing of a torus into a formal representation of $\mathbb{T}^2$

[Jiatong Yang]

Thank you. What should do I to improve my Lean skills? (I'm now learning the tutorials and solving problems on codewars)

[Arthur Paulino]

It depends on your goal. How do you plan to use Lean?

If you want to use it for proving mathematics, then get involved with mathlib in Lean 3 I think.

If you want to get good at programming with Lean, then creating libs for Lean 4 might be suitable.

If you want to learn about metaprogramming, then helping out with the mathlib port to Lean 4 might be a good opportunity. At the very least, you shall learn about Syntax, TacticM and MetaM

[Jiatong Yang]

I'd like to use it for proving mathematics. Thank you for your suggestions! :heart:

[Moritz Doll]

what kind of mathematics are you interested in?

[Martin C. Martin]

Is Theorem Proving in Lean still considered a good way to start? Mathematics in Lean? Logic and Proof? Some other tutorials or exercises? Which ones?

[Moritz Doll]

TPiL is more a reference manual, Mathematics in Lean has recently got some additions, so you might want to look into that. If you are interested in what is in mathlib already or what would be a suitable area to contribute to, then you should look into the documentation of mathlib itself or ask here

[Moritz Doll]

this page is still very much accurate: https://leanprover-community.github.io/learn.html

[Moritz Doll]

(maybe one could add a link to the LftCM22 videos)

[Jiatong Yang]

Moritz Doll said:

what kind of mathematics are you interested in?

I'm not sure about that because I'm not yet an undergraduate. :joy: I've only learned the very basics of mathematics.

[Jiatong Yang]

I've read the tutorial project, theorem proving in Lean, Lean references, Logic and Proof. But I still have great difficulty doing 5-kyu or 6-kyu problems on codewars.

[Moritz Doll]

Oh then you should definitively first learn informal mathematics (we have some undergrads that learned mathematics with lean, but this is very exceptional)

[Jiatong Yang]

I've seen in mathlib propositions are generalized very far. For example, it uses filter to define limits :flushed: .

[Jiatong Yang]

Now ITP is just a hobby of mine and I hope it will help with my maths later.

[Huỳnh Trần Khanh]

not yet an undergraduate

You must be the cream of the crop then.

[Jiatong Yang]

You are flattering me :joy: . I just got to know functional programming early this year and was attracted by ITP.

[Anatole Dedecker]

Jiatong Yang said:

Now ITP is just a hobby of mine and I hope it will help with my maths later.

Speaking from my experience, if you've done the tutorial project, this might already help you a lot with classical maths !

[Junyan Xu]

Mario Carneiro said:

I will be very impressed if a program manages to interpret my shitty drawing of a torus into a formal representation of $\mathbb{T}^2$

They have donut as a category but not torus ...

[Winston Yin]

Oh then you should definitively first learn informal mathematics (we have some undergrads that learned mathematics with lean, but this is very exceptional)

As someone who learned Lean and formalisation long after completing my maths degree, I would say that you have the unique opportunity to go through a standard maths curriculum with computer formalisation in mind.

Thinking about type theory at all while learning basic mathematical ideas is something few maths undergrads have the luxury of doing.

As you learn the informal definitions and theorems about metric spaces, groups, etc, you may reference how mathlib expresses them in type theory language. For me, it has clarified my understanding of exactly which properties of such structures lead to our favourite theorems about them. The experience is no less illuminating than learning point set topology after normed spaces.