Lean 4 status

Stream: general

[Bjørn Kjos-Hanssen]

So... how many % done is the mathlib translation from Lean 3 to Lean 4 at this point?
Specifically I'm wondering how hard it would be to translate files like these now: https://github.com/bjoernkjoshanssen/diophantine-lemma

[Jireh Loreaux]

100%

[Jireh Loreaux]

You should use mathport to translate them.

[Eric Wieser]

You are probably going to have a bad time translating a lean non-project like that repo; you should first add a leanpkg.toml and get it all building on current mathlib

[Martin Dvořák]

I was today years old when I learnt that 2x+3y=7.lean is a valid filename.

[Kevin Buzzard]

Can you import it though?

[Ruben Van de Velde]

Probably with «»

[Bjørn Kjos-Hanssen]

Martin Dvořák said:

I was today years old when I learnt that 2x+3y=7.lean is a valid filename.

And I was today years old when I learned that so is 7.lean=2x+3y, so equality may be commutative.