Lean4 vs Lean3

Stream: new members

[Byung-Hak Hwang]

Hello! I've just started studying formalization and Lean4, and I have two quick questions:

1. What are the advantages of Lean4 over Lean3?
2. From what I understand, when formalizing math began, many people used Lean3, so thousands of math theorems were written in Lean3. After Lean4 was developed, I heard that the project to convert these math libs into Lean4 was completed last year. How did the community manage this conversion? Is there an auto-translator from Lean3 to Lean4?

[Henrik Böving]

1. Its faster, has lots of new features, is a proper programming language as well if you are interested in that. And unlike lean 3 the community actually uses it right now and it is still being developed
2. There does exist a partial auto converter, most of it was people running that and then cleaning up the input by hand.

[Yaël Dillies]

Henrik Böving said:

1. then cleaning up the input by hand

*output!

[Byung-Hak Hwang]

Henrik Böving 말함:

1. Its faster, has lots of new features, is a proper programming language as well if you are interested in that. And unlike lean 3 the community actually uses it right now and it is still being developed
2. There does exist a partial auto converter, most of it was people running that and then cleaning up the input by hand.

Thank you for clear answers! Is the partial converter available for public use? I'm curious about how the converter handles the grammar of Lean3 and Lean4.

[Markus Himmel]

Yes, see https://github.com/leanprover-community/mathport

[Byung-Hak Hwang]

Markus Himmel 말함:

Yes, see https://github.com/leanprover-community/mathport

Great! I'll check the GitHub page. Thank you.