Mathlib on Lean4 when?

Stream: lean4

[Thomas Browning]

My understanding is that there's a sort of 2-step approach:
Step 1: Get mathlib ready in the form of mathport PRs: https://github.com/leanprover-community/mathlib/pulls?q=is%3Apr+label%3Amathport
Step 2: A tool along the lines of https://github.com/dselsam/mathport/
See also: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport
But I'm not familiar with this stuff, so someone more qualified should chime in

[Yury G. Kudryashov]

Note that mathport builds Lean4 oleans from Lean3 files, not Lean4 source files. As far as I understand, once mathlib is mathport-ready we can try to start mixing Lean3 and Lean4 code. But we'll need to port the source files in some order. As a person who knows how to write proofs but knows almost nothing about meta programming in lean (OK, I fixed some bugs in to_additive but that did not involve any deep understanding of what's going on) I think that the most challenging part is to port the tactic folder and reimplement features like old_structure_cmd.

[SnowFox]

Ohhh. Very nice approach. Thanks.

[Yury G. Kudryashov]

Disclaimer: I may be wrong.

[Daniel Selsam]

Yes, mathport automatically creates Lean4 .olean files for each Lean3 file. It does not port meta Lean though, and so most mathlib tactics will need to be manually ported to Lean4. Mathport is a simple program and most of the work right now is:

• mathlib community backporting a few Lean4 features
• Leo finalizing a few Lean4 design decisions (some backports may or may not be necessary depending)

The issues are being tracked here: https://github.com/dselsam/mathport

After resolving these known issues, I will re-run the tool and do another round of experiments to look for additional issues. Once we are confident that the auto-ported .oleans are stable and usable (except for missing tactics), we enter Phase 2.

Phase 2 is porting the basic tactics, including some that may depend on parts of the auto-ported mathlib. Some tactics will no longer be necessary thanks to more flexible Lean4 built-in tactics, some others will be obviated by decision procedures Leo is planning to implement, and some others are rarely used and can be delayed to Phase 3. But this phase may still require a significant amount of work.

There is no official consensus yet for what happens in Phase 3. There are two main proposals that I know about:

Proposal 1 (Incremental):

- encourage most people to do most new things in Lean4 on top of the auto-ported .oleans
- incrementally replace the Lean4 .oleans with .lean files starting at the leaves
- as necessary, refactor in Lean3, re-run the auto-porter and propagate the changes
- possibly even have tooling support for multi-lean projects

Proposal 2 (Abrupt):

- once the tools are ready to recreate Lean4 .lean files efficiently, freeze mathlib3
- mobilize community-wide effort to port as much as possible before allowing new math
- require that every .lean file expose the exact same API as the .olean so that porting becomes embarrassingly parallel
- possibly schedule this for 1 month over the summer, when people are less likely to have other deadlines

I advocate Proposal 2 due to the strong network effects of concentrating tooling on a single system and the significant costs (both hidden and visible) of multi-language projects. However, which proposal makes the most sense depends a lot on how much work it takes to reconstruct a .lean file. This process may turn out to be not-so-bad thanks to the delaborator. It might also be possible to implement a special-purpose heuristic delaborator just for this use-case that recovers most rewrite/simp/cases/induction/obtain tactics from the low-level proof terms. If the reconstructed .lean files really have the exact same API as the .olean files, it may also make sense to allow difficult proofs to persist temporarily as binary proof terms in separate files.

[Scott Morrison]

Proposal 2 so far feels unrealistic to me. I'm having trouble imagining a delaborator that could produce human-plausible tactic blocks (or make reasonable judgements e.g. about which arguments to omit in favour of _ in term mode proofs). Every single line in mathlib is going to need human review, surely. And most nontrivial tactic blocks will require human editing.

[Scott Morrison]

In any case, if there is useful work that can be done by people who know mathlib well, but are not yet regular Lean4 users (e.g. me), it would be great to have this farmed out. I'm very keen to make the transition, but as I understand there's not so much to be done yet.

[Scott Morrison]

At https://github.com/dselsam/mathport#contributing you say:

The best way to help is to find and isolate issues. Pick your favorite mathlib file, start reimplementing it in Lean4, and file (small, isolated) GitHub issues for any specific pain points you encounter.

Could you explain in more detail what you mean here? Which files are most plausible to try?

[Daniel Selsam]

Scott Morrison said:

At https://github.com/dselsam/mathport#contributing you say:

The best way to help is to find and isolate issues. Pick your favorite mathlib file, start reimplementing it in Lean4, and file (small, isolated) GitHub issues for any specific pain points you encounter.

Could you explain in more detail what you mean here? Which files are most plausible to try?

@Scott Morrison I have not run mathport since a few of the backports got merged into mathlib. I will re-run the pipeline tomorrow, articulate exactly what is still not expected to work yet, and clarify the contributor suggestions.