What do we know about Lean 4?

Stream: general

[Yury G. Kudryashov]

Hi, I wonder what should I (as a user) expect from Lean 4 and Lean 3 → 4 porting of mathlib. While I found some slides about new core features coming to Lean 4, I failed to find answers to some basic questions.

What about compatibility?

• Do I guess correctly that most of the tactic code in mathlib will have to be rewritten to work with Lean 4?
• What about proofs / theorems / defs?

Algebraic classes (monoids, groups, etc)

Are there any big changes coming here?

What should I expect from porting?

Is it going to be "let's feature freeze and port to Lean 4", "let's start a new branch gradually pick files from master", "let's gradually make parts of the library compatible with Lean 4 while maintaining compatibility with Lean 3", or something else?

[Yury G. Kudryashov]

I ask this to avoid spending too much time on the parts of mathlib that are going to be rewritten from scratch.

[Patrick Massot]

Many answers are unknown, but there are a couple of facts:

• Leo never promised any compatibility between Lean 3 and Lean 4. In fact he very explicitly warned everybody there won't be any compatibility, and we shouldn't build anything and expect it to work in Lean 4. He is on a mission to build a better proof assistant. He always writes this is a research project and not a product.
• Everything we do nonetheless in Lean 3 is worthwhile. The type class instance resolution procedure of Lean 4 has been developed using the experience gathered in mathlib. This is crucial.
• The tactic framework of Lean 4 doesn't exist yet, but one can be sure that not a single line of mathlib tactic code will work without modification in Lean 4.

Less certain pieces include:

• Personally I think the community of mathematicians using Lean 3 is a huge success that will survive Lean 3.
• It may be possible to write code which automates at least partly the conversion of Lean 3 to Lean 4. I think the dream is that the Lean 4 parser will be flexible enough to parse Lean 3 code and output an approximate Lean 4 version.
• The mathlib community does not have a fixed plan for the transition. There cannot be a plan as long as we don't know more about the preceding point.
• I don't see any reason why mathlib would be more centralized than it currently is. There is no dictator who will say: mathlib is now frozen, everybody should work on porting. Everybody will continue doing whatever they want using whatever time they can find. We may have rules like: don't port and modify a file at the same time, since this could make a huge mess and create a lot of additional work.

[Patrick Massot]

The safest bet if you want to work on something that will stay is documentation.

[Patrick Massot]

You can pick a random file which has no header and docstrings and document it.

[Patrick Massot]

Or, better: write a Windows installer!

[Yury G. Kudryashov]

I'm afraid my instructions for installing something on a WIndows computer would start with "install Linux".

[Patrick Massot]

That's how my instructions start, but experience proved this is not enough.

[Patrick Massot]

This is really bad luck. Last year most of my students had Linux at the end of the semester, because they were forced to install it by computer scientists (I'm using Lean with double-major math/CS students). But I need them to start using Lean at the beginning of the semester.

[Yury G. Kudryashov]

BTW, what changed about class instance resolution in Lean 4?

[Kevin Buzzard]

The algorithm completely changed but as far as I know the new one hasn't been implemented yet

[Patrick Massot]

I think it has been implemented, at least partly.

[Yury G. Kudryashov]

Is there any paper/presentation/... describing the new algorithm?

[Kevin Buzzard]

As far as I know there are just posts by Daniel Selsam on this chat, e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/instances.20and.20parameters/near/178623928

[Simon Hudon]

The algorithm completely changed but as far as I know the new one hasn't been implemented yet

They're in the middle of reimplementing it now

[Sebastian Ullrich]

Algebraic classes (monoids, groups, etc)

Are there any big changes coming here?

I don't think I have anything new to share about the other questions, but this one should be easy to answer: AFAIK the plan is not to include the algebraic hierarchy in the corelib, since there is no reason to do so. So this will be up to the community.

[Mario Carneiro]

what's going to happen with tactic.norm_num and the algebraic dependencies there?

[Sebastian Ullrich]

There should be no reason to include norm_num in the corelib, either