Zulip Chat Archive

Stream: lean4

Topic: Mathlib on Lean4 when?


view this post on Zulip Thomas Browning (Mar 16 2021 at 21:27):

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

view this post on Zulip Yury G. Kudryashov (Mar 16 2021 at 22:27):

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.

view this post on Zulip SnowFox (Mar 16 2021 at 22:45):

Ohhh. Very nice approach. Thanks.

view this post on Zulip Yury G. Kudryashov (Mar 17 2021 at 01:54):

Disclaimer: I may be wrong.

view this post on Zulip Daniel Selsam (Mar 17 2021 at 03:29):

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.

view this post on Zulip Scott Morrison (Mar 17 2021 at 03:40):

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.

view this post on Zulip Scott Morrison (Mar 17 2021 at 03:42):

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.

view this post on Zulip Scott Morrison (Mar 17 2021 at 03:48):

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?

view this post on Zulip Daniel Selsam (Mar 17 2021 at 04:01):

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.


Last updated: May 07 2021 at 12:15 UTC