can lean express any kind of mathematics?

Stream: new members

[Anh Nguyễn]

I am new to this community and I want to have an overview about Lean

[Matt Diamond]

Do you have a specific question or are you just looking for documentation?

[Anh Nguyễn]

Matt Diamond said:

Do you have a specific question or are you just looking for documentation?

My question is in principle, Lean can express any kind of mathematics, right?

[Notification Bot]

3 messages were moved here from #new members > hello? by Matt Diamond.

[Matt Diamond]

(@Anh Nguyễn I hope you don't mind but I moved your messages to this new thread.)

[Bjørn Kjos-Hanssen]

Yes, it can.

[Bjørn Kjos-Hanssen]

First-order logic is represented within Lean, which should be enough for anything.

[Anh Nguyễn]

Matt Diamond said:

(Anh Nguyễn I hope you don't mind but I moved your messages to this new thread.)

Bjørn Kjos-Hanssen ☀️ said:

Yes, it can.

No matter how complex it is, right?

[Derek Rhodes]

@Anh Nguyễn, if you're still looking for an overview of Lean and Mathlib, then a good place to start is over on this page:

https://leanprover-community.github.io/learn.html
From there, I think most people start with the Natural Number Game.

[Anh Nguyễn]

Derek Rhodes said:

Anh Nguyễn, if you're still looking for an overview of Lean and Mathlib, then a good place to start is over on this page:

https://leanprover-community.github.io/learn.html
From there, I think most people start with the Natural Number Game.

Thank you for your suggestion

[Anh Nguyễn]

Is it true that a proof is just navigating through statements

[Anh Nguyễn]

similar to a game?

[Bjørn Kjos-Hanssen]

Yes, it's true. However, every unsolved problem in mathematics (such as this one) can be viewed as a "level" in this game, so some "levels" of this game are impossibly hard.

[Anh Nguyễn]

Bjørn Kjos-Hanssen ☀️ said:

Yes, it's true. However, every unsolved problem in mathematics (such as this one) can be viewed as a "level" in this game, so some "levels" of this game are impossibly hard.

So there always exist the "path" to any theorem, right?

[Anh Nguyễn]

Anh Nguyễn said:

Bjørn Kjos-Hanssen ☀️ said:

Yes, it's true. However, every unsolved problem in mathematics (such as this one) can be viewed as a "level" in this game, so some "levels" of this game are impossibly hard.

So there always exist the "path" to any theorem, right?

Thank you, i got it

[Anh Nguyễn]

could Lean attack open problems right now?

[Eric Wieser]

That question is perhaps a little bit like "can $\LaTeX$ attack open problems" - you can certainly use Lean to attack open problems, but it will be you the driver doing the vast majority of the attacking.

[Anh Nguyễn]

Eric Wieser said:

That question is perhaps a little bit like "can $\LaTeX$ attack open problems" - you can certainly use Lean to attack open problems, but it will be you the driver doing the vast majority of the attacking.

I mean when it is powered with AI

[Anh Nguyễn]

Eric Wieser said:

That question is perhaps a little bit like "can $\LaTeX$ attack open problems" - you can certainly use Lean to attack open problems, but it will be you the driver doing the vast majority of the attacking.

I'm sorry for not being clear enough

[Anh Nguyễn]

Has anyone tried AI with research-level mathematics?

[Damiano Testa]

You can take a look at #Machine Learning for Theorem Proving, but there are lots of other discussions elsewhere as well.

[Anh Nguyễn]

Damiano Testa said:

You can take a look at #Machine Learning for Theorem Proving, but there are lots of other discussions elsewhere as well.

Thank you for suggesting

[Anh Nguyễn]

image.png

[Anh Nguyễn]

I saw this image

[Anh Nguyễn]

and I am wondering about what is the current state