Zulip Chat Archive

Stream: lean4

Topic: mathlib


view this post on Zulip Kenny Lau (Jan 05 2021 at 15:25):

is there a mathlib for lean 4 yet? as in, a place to port lean 3 mathlib to

view this post on Zulip Kenny Lau (Jan 05 2021 at 15:26):

@Mario Carneiro I heard that you're working on logic.basic

view this post on Zulip Mario Carneiro (Jan 05 2021 at 15:26):

working is a strong word

view this post on Zulip Mario Carneiro (Jan 05 2021 at 15:26):

There is certainly no place to port mathlib yet, and I think that's still premature

view this post on Zulip Mario Carneiro (Jan 05 2021 at 15:27):

I think for the present we should be doing single file experiments

view this post on Zulip Kenny Lau (Jan 05 2021 at 15:27):

what do you have now?

view this post on Zulip Mario Carneiro (Jan 05 2021 at 15:27):

~nothing

view this post on Zulip Kenny Lau (Jan 05 2021 at 15:30):

Well at least it would be better if there's an empty repository on github that has Lean 4 environment

view this post on Zulip Aaron Anderson (Jan 05 2021 at 19:16):

Is it too early to start threads to discuss design changes to mathlib that could be implemented during the port?

view this post on Zulip Kenny Lau (Jan 05 2021 at 19:21):

I think we should get logic.basic working first

view this post on Zulip Bryan Gin-ge Chen (Jan 05 2021 at 19:23):

Zulip threads are cheap, so I would say no; it's not too early. Proposals with supporting evidence from code experiments will of course be more useful, and it will also take some time before enough people are comfortable with Lean 4 for there to be much feedback.

(I agree that porting logic.basic is a reasonable first milestone.)

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 19:35):

It's the logic.basic game!

view this post on Zulip Johan Commelin (Jan 05 2021 at 19:51):

Johannes Holzl used to warn against mixing porting and design changes. He said you would fail on both parts if you tried that.

view this post on Zulip Eric Wieser (Jan 05 2021 at 20:01):

I can't see full porting ever happening unless we either:

  • Work out a compatibility layer, like how the python ecosystem ran against both 2 and 3 with the same source code.
  • Freeze the lean3 mathlib
  • Automate the translation (a la 2to3.py)

Is there a path I'm missing?

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 20:02):

Manual porting over the next few years

view this post on Zulip Daniel Selsam (Jan 05 2021 at 20:03):

I am planning to implement a preliminary version of the tool Leo suggested yesterday, with the hope that it will be easy enough for the community to tweak and extend as desired.

view this post on Zulip Bryan Gin-ge Chen (Jan 05 2021 at 20:03):

(For reference, here's the relevant timestamp to Leo's talk)

view this post on Zulip Kevin Lacker (Jan 05 2021 at 20:05):

which tool do you mean Daniel - a tool to let include both lean 3 and lean 4 files in the same build, or a tool to export lean 3 things to lean 4?

view this post on Zulip Daniel Selsam (Jan 05 2021 at 20:13):

Kevin Lacker said:

which tool do you mean Daniel - a tool to let include both lean 3 and lean 4 files in the same build, or a tool to export lean 3 things to lean 4?

  1. add functionality to Lean3 to allow exporting the declarations plus metadata such as typeclass instances and notation in (say) a foo.lean3port file for each foo.lean
  2. a stand-alone executable that transforms .lean3port files into the .olean format that Lean4 can import.

view this post on Zulip Reid Barton (Jan 05 2021 at 20:20):

Aaron Anderson said:

Is it too early to start threads to discuss design changes to mathlib that could be implemented during the port?

I'd say instead: it's not too late to start threads about design changes that could be implemented before the port :upside_down:

view this post on Zulip Reid Barton (Jan 05 2021 at 20:26):

@Gabriel Ebner had a similar tool described here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Importing.20mathlib.20into.20Lean.204/near/187561178

view this post on Zulip Eric Wieser (Jan 05 2021 at 20:29):

Presumably we'll want a tool in both directions if we're starting from logic.basic - otherwise we'd have to start at the other end

view this post on Zulip Eric Wieser (Jan 05 2021 at 20:29):

That is, importing lean 4 data into lean3 source files

view this post on Zulip Daniel Selsam (Jan 05 2021 at 20:32):

Reid Barton said:

Gabriel Ebner had a similar tool described here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Importing.20mathlib.20into.20Lean.204/near/187561178

Thanks, looking at it now. It seems like the two things missing (besides all the tweaks I wasn't planning to add) are:

  • don't require a monolithic import, and instead do this for each file individually
  • export more metadata, in particular instances and notation

view this post on Zulip Eric Wieser (Jan 05 2021 at 20:39):

Is "exporting instances" anything other than exporting attributes?

view this post on Zulip Gabriel Ebner (Jan 05 2021 at 21:00):

My importer tool actually handles classes, instances, and simp lemmas. (There's a separate text file for the additional metadata).

view this post on Zulip Gabriel Ebner (Jan 05 2021 at 21:06):

The hard parts are:

  1. Recursors are now different. (The construction of the old recursor is not hard, but you to invent a new name, etc.)
  2. I think it's important to map at least some core definition to the Lean 4 equivalent, such as natural numbers, logical constants, decidability, etc. Otherwise the imported library is basically impossible to use. A lot of stuff maps directly, but it's a chore to list all the new names.
  3. However many definitions in core were already different when I wrote the tool. Now the core library has diverged even further. (Think HasCoe, or numerals, etc.)
  4. Some definitions no longer check because of subtle changes in the type checker. (Think large numerals, e.g. in unsigned.) This should be trivial to fix when porting manually, but in an automatic tool it's a nasty curveball.

view this post on Zulip Kenny Lau (Jan 05 2021 at 21:51):

my current translation of the very beginning of logic.basic:

universes u v

/-- Ex falso, the nondependent eliminator for the `Empty` type. -/
def Empty.elim {C : Sort u} (t : Empty) : C := nomatch t

instance : Subsingleton Empty := λ a => a.elim

instance {α : Type u} {β : Type v} [Subsingleton α] [Subsingleton β] : Subsingleton (α × β) :=
λ a₁, b₁ a₂, b₂ => congr (congrArg _ $ Subsingleton.elim _ _) (Subsingleton.elim _ _)⟩

instance : DecidableEq Empty := λa => a.elim

instance instSortInhabited' : Inhabited (Inhabited.default : Sort u) := PUnit.unit

instance decidableEqOfSubsingleton {α : Sort u} [Subsingleton α] : DecidableEq α :=
fun a b => isTrue (Subsingleton.elim a b)

@[simp] theorem eqIffTrueOfSubsingleton [Subsingleton α] (x y : α) : x = y  true :=
λ _ => _⟩, λ _ => Subsingleton.elim x y

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 22:35):

Porting has officially begun :D

view this post on Zulip Adam Topaz (Jan 05 2021 at 22:36):

So where's the repo? :smile:

view this post on Zulip Bryan Gin-ge Chen (Jan 05 2021 at 23:01):

Rather than creating a new community repo and reinviting everyone, for now I think we could create one (or several) orphan branches in the mathlib repo for Lean 4 experiments. These branches won't share any history or files with the Lean 3 mathlib (so CI won't run on them).

Instructions (copied from this SO post):

git checkout --orphan my_lean4_experiment
git rm -rf .
<do work>
git add your files
git commit -m 'Initial commit'

view this post on Zulip Bryan Gin-ge Chen (Jan 05 2021 at 23:03):

Then anyone can add commits to these branches as usual. leanproject get-cache won't work on these branches (until we set up some kind of CI), so anyone checking out such a branch will have to compile everything themselves.

view this post on Zulip Bryan Gin-ge Chen (Jan 05 2021 at 23:04):

(Feel free to point out reasons why this might be a terrible idea...)

view this post on Zulip Alex Peattie (Jan 05 2021 at 23:12):

If there's no CI/olean compilation concerns, I guess a Lean 4 mathlib repo could theoretically use the "normal" model for a Github repository. E.g. a repo with the maintainers invited, but then people work on forks + PRing rather than pushing their branches to the main repo? Which would mean no worries about reinviting everyone? Although I think orphan branches is a certainly clever approach if the preference is to avoid a new repo :smile:

view this post on Zulip Daniel Selsam (Jan 06 2021 at 02:16):

Has anyone made a back-of-the-envelope estimate of how much time it would take to just port Mathlib manually, bottom-up? Here is a heavily-simplified first attempt:

Assuming:

  • 50,000 theorems
  • 100 collaborators
  • X minutes on average to port a theorem (this has high variance)
  • 40 hour work-weeks

It would take:

  • 500 theorems per person
  • 500 * X minutes per person
  • 500 * X / (60 * 40) weeks in total

After an initial investment to write Lean3-parity tactics/automation in Lean4 (which will presumably be necessary anyway), what would be a good estimate for X? 2? 5? 10? Even if X is 10, the porting would only take two weeks under this model. Even if a better model predicted 2 months, it might still be worth just pulling off the band-aid. Note: I am not suggesting this approach, only floating the idea.

view this post on Zulip Huỳnh Trần Khanh (Jan 06 2021 at 02:20):

I think we should be using some sort of automation, maybe parse the current mathlib into some sort of abstract syntax tree and then visit that syntax tree to emit Lean 4 code. https://blog.isquaredsoftware.com/2018/11/git-js-history-rewriting/

view this post on Zulip Huỳnh Trần Khanh (Jan 06 2021 at 02:22):

At the end of the day there would many steps that are purely mechanical and doing them by hand would be a waste of time.

view this post on Zulip Daniel Selsam (Jan 06 2021 at 02:26):

Yes, there is a lot that could be done automatically, though I expect the porting time will be dominated by the time it takes to fix the tactic scripts that (even after syntactically adjusting them) no longer work for subtle reasons.

view this post on Zulip Jason Rute (Jan 06 2021 at 02:34):

As someone who has written automation to parse proofs into abstract syntax trees, it is really hard to do. Lean's grammar is dynamic and only Lean can truly parse Lean. One option is to modify the current C++ Lean 3 parser to output the needed information.

Or, we were able to get pretty far by hacking into to parts of the Lean parsing framework and writing a light weight parser to get the rest of the way there. (It would also be possible to build on the current C++ Lean 3 parser to get this data as well.) I'm happy to share what we have when it's ready. We don't have ASTs for the whole file, just for tactic proofs and we don't parse expressions (which one would have to change because of capitalization changes). We just store the expressions as strings right now. I'm not sure if this would be helpful or not (especially in light of Daniel's comments).

view this post on Zulip Joe Hendrix (Jan 06 2021 at 02:42):

I'm wondering how feasible it would be to adopt an incremental approach where files in Lean 3 are incrementally "frozen" in Lean 3 and then ported to Lean 4. Once a given file is done, you shouldn't merge any PR changes into those files, but before then, it's ok to keep working on the Lean 3 versions. If you are predominantly working in certain files, then you could migrate to Lean 4 once they are ported. A file would only be eligible for freezing after all it's imports are.

view this post on Zulip Huỳnh Trần Khanh (Jan 06 2021 at 02:50):

That sounds a lot like the "strangler pattern".

view this post on Zulip Daniel Selsam (Jan 06 2021 at 03:19):

@Joe Hendrix One risk for any incremental approach is a bad Nash-equilibrium. I fear that individuals may not have sufficient incentive to invest heavily in Lean4 until they are confident that others will as well. In the 'pulling off the band-aid' approach, the community-optimal incentives could be achieved immediately by a community decision to freeze mathlib3 and to port to Lean4 before resuming business-as-usual.

view this post on Zulip Joe Hendrix (Jan 06 2021 at 05:33):

I was thinking kinda thinking that it would be good to let people interested in formalizing particular theories continue to do so while the more fundamental building blocks (e.g., decision procedures, logical foundations) are ported. The collective community decision though would be that Lean 3 versions are not to be updated for any reason once the Lean 4 porting of those versions is underway.
There could be a long tail of porting various particular contributions over with this though, so maybe there would be a deadline associated with freezing the entire codebase.
I'm not familiar with the strangler pattern, but I wasn't thinking about intermingling the ability to use Lean 3 within Lean 4 (or vice versa).

view this post on Zulip Johan Commelin (Jan 06 2021 at 05:35):

@Daniel Selsam the problem with your calculation is that it only works if you can port file xyzzy even though you don't know what its ported dependencies foo, bar, and quux look like. You can do it with 100 people in two weeks if you can parallelise the tasks. But I don't know if that is true.

view this post on Zulip Johan Commelin (Jan 06 2021 at 05:36):

We had a lintsprint two months ago. That worked well, with say 10-15 people contributing several PRs a day. But there were no interdependencies between those PRs.

view this post on Zulip Johan Commelin (Jan 06 2021 at 05:37):

So, if we can get lean 4 to work with special .lean3olean_plus_mathlib_metadata files, then we might be able to parallelise the porting effort.

view this post on Zulip Johan Commelin (Jan 06 2021 at 05:37):

Also, as warned above, porting would need to be very very strict, otherwise the parallelism will break. Everytime you see some bad design, leave a comment, but copy it faithfully. People importing your file will thank you later.

view this post on Zulip Johan Commelin (Jan 06 2021 at 08:04):

Daniel Selsam said:

Assuming:

  • 50,000 theorems
  • 100 collaborators
  • X minutes on average to port a theorem (this has high variance)
  • 40 hour work-weeks

It would take:

  • 500 theorems per person
  • 500 * X minutes per person
  • 500 * X / (60 * 40) weeks in total

Also, I don't think 100 people will invest 2 weeks of 40 hours in porting stuff. In Feb/March I can probably invest 3 full weeks, but I guess I'm an exception. So it will probably be more like 10 people working for 20 weeks... and then, I don't have 20 weeks that I can work nonstop on this project.

view this post on Zulip Patrick Massot (Jan 06 2021 at 08:36):

I guess the olean export/import is what is meant to allow parallelism. But I also think that some kind of automatic preliminary translation of statements would be nice (tactic proofs are probably hopeless and for term proofs we want to use the new features of Lean 4 to kill @ _ _ _ _).

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:04):

My two cents here:

Some of us remember the old days when Lean was always changing underneath us, and we all know the "bump Lean to 3.24.0c" PRs to mathlib. These can be painful, and Lean 4 is brand new and presumably in flux. This is fine, even good. It's a sign the system is improving. But it adds tremendously to the cost of a port.

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:04):

I don't think we should start a full port now, or even necessarily soon. It's time to experiment. And there are a number of experiments to do, all somewhat independent.

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:04):

One is what Leo suggested in his talk: import Lean 3 mathlib with metadata and try to build on that, or port files at the top of the import hierarchy. This gives very important information about how Lean 4 features will scale. There was a lot about Lean 3 that we didn't learn until mathlib got big.

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:05):

This is a really important experiment but I'm skeptical about it as a long-term survival strategy for mathlib. IMO the Frankenstein approach will be harder to maintain and much harder for new contributors to wrap their heads around. The community development style is an essential part of mathlib and if we arrive at something that we can't teach newcomers, we've lost the game.

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:05):

Two is what people started yesterday, just start porting things from the ground up. Learn Lean 4 syntax and bug hunt on smaller proofs. This is totally independent of the first approach. As I said, I think it's too early to dump everyone's full effort into doing this. But carving out an initial chunk -- logic.basic, some of algebra, core pieces of data -- will be really helpful, especially to see the effects of the inevitable changes to Lean 4.

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:05):

Three, there's the 20k loc in tactic. Any kind of automated porting here seems hopeless. Many mathlib tactics are basically just linguistic things (obtain, set, etc) that might even be two-line macros in Lean 4. ring, linarith, slim_check, etc will be hard to port. (Leo said he plans to implement a version of linarith himself at some point.) The current omega is almost certainly dead. For a native Lean 4 mathlib, we need versions of most of this. Porting tactics isn't completely independent of the second approach, but I think it can be started independently. And as before, we should experiment with metaprogramming before committing to porting the big stuff.

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:05):

So I'd like to see three experiments done in parallel and independently. These can help us in the future but none is expected to be the future. Lean 3 mathlib development can continue in Lean 3, albeit likely at a slower pace if people are directing their time to the porting effort. After some iteration on these experiments, we'll have a better idea how to approach a full port. In particular we'll have more accurate numbers for Daniel's time estimate.

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:05):

(Sorry for the essay!)

view this post on Zulip Patrick Massot (Jan 06 2021 at 09:07):

Don't forget to add experimentation with rebuilding the basic algebraic hierarchy (without proving any lemma) using the structure command provided by Lean4 or a new new structure command somewhat simulating the old structure command using the new one. Or even try to rebuild it using unification hints!

view this post on Zulip Gabriel Ebner (Jan 06 2021 at 09:15):

I mostly agree with Rob, except that the critique of Frankenlean's monster maybe misses the point a bit. The motivation behind a hybrid Lean 3 / Lean 4 mathlib is as a viable temporary transition strategy. Porting mathlib is gonna take a few months. We know from linting sprints that we can organize incremental library cleanups. I am not sure we can pull off having two separate repositories.

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:20):

I don't see how we achieve a full port top-down, but I'd be happy to be proven wrong.

view this post on Zulip Eric Wieser (Jan 06 2021 at 09:21):

I fear the rate at which mathlib is ported will be slower that the rate at which the lean3 version grows - so a multiple repository approach seems like it wouldn't work, and a hybrid approach is the only option.

view this post on Zulip Eric Wieser (Jan 06 2021 at 09:21):

Can we strive for a bottom-up port instead?

view this post on Zulip Alex J. Best (Jan 06 2021 at 09:24):

Eric Wieser said:

I fear the rate at which mathlib is ported will be slower that the rate at which the lean3 version grows - so a multiple repository approach seems like it wouldn't work

I wonder if there are some areas of interest to mathlib that are not well represented in mathlib so far (and so have few serious dependecies). People could start working on some of these from almost nothing in a mathlib 4, such projects might be a fun way for the community to learn lean 4 that isn't just porting existing work.

view this post on Zulip Johan Commelin (Jan 06 2021 at 09:27):

numerical analysis?

view this post on Zulip Johan Commelin (Jan 06 2021 at 09:27):

see the undergrad page, there are several sections that are just empty

view this post on Zulip Mario Carneiro (Jan 06 2021 at 09:48):

Eric Wieser said:

I fear the rate at which mathlib is ported will be slower that the rate at which the lean3 version grows - so a multiple repository approach seems like it wouldn't work, and a hybrid approach is the only option.

Once the porting gets far enough, it will be stable enough that people can feel comfortable writing new things in lean 4 mathlib, so the rate of lean 3 mathlib contributions will plateau and eventually dwindle

view this post on Zulip Mario Carneiro (Jan 06 2021 at 09:49):

But I definitely think that porting will take far too long for a global freeze to be viable

view this post on Zulip Mario Carneiro (Jan 06 2021 at 09:51):

Freezing at a file level is maybe doable, although I don't think it's particularly necessary, since the changes that happen to a given file are usually pretty low frequency. We have done lint sprints and other refactorings at about this level of disruptiveness already in the past

view this post on Zulip Sebastien Gouezel (Jan 06 2021 at 11:15):

Mario Carneiro said:

But I definitely think that porting will take far too long for a global freeze to be viable

Once all tactic files and all basic algebra files are ported, I wouldn't be surprised if the port were essentially mechanical. Maybe I'm too optimistic, but I guess we will stumble all the time on the same issues, so once we know how to fix these I don't see why it wouldn't be pretty smooth.

view this post on Zulip Mario Carneiro (Jan 06 2021 at 13:38):

I think it is definitely worth the time to set up the means to make it as mechanical as possible, but I don't think we will be able to reduce the manual part of the porting to zero. A few files a day seems like an upper limit on the amount of work one person could get done if it's all going smoothly, so together with the PRs and coordination I think a few months sounds about right

view this post on Zulip Simon Hudon (Jan 06 2021 at 18:19):

In terms of new designs for mathlib, after the port, it would be valuable to move tactics into a separate packages so that we can run them in mathlib in compiled form. (unless Leo implements just-in-time compilation) That will likely be a big change.

view this post on Zulip Kevin Lacker (Jan 06 2021 at 21:26):

in my experience with porting projects, they fail not when there is too much overall work, but when there are 2 or 3 critical things that are so hard to port, the people working on it eventually give up and nobody wants to try any more. so I am curious what are the hardest parts of mathlib to port, that are critical for mathlib. is it complex but commonly used tactics like ring, omega, simp, linarith, etc?

view this post on Zulip Joe Hendrix (Jan 06 2021 at 21:27):

I haven't thought through the implementation, but it seems like it should be possible to compile tactics in one module and use the compiled version in other modules without a JIT. I think this would result in using the compiled versions in most cases.

view this post on Zulip Bryan Gin-ge Chen (Jan 06 2021 at 21:27):

Lean 4 has a simplifier, but all the other tactics you mentioned will have to be ported.

view this post on Zulip Mario Carneiro (Jan 06 2021 at 22:32):

For most tactics, I expect that we can port them just like we port other things. That said I would bet that we want to make more significant changes to some of them: omega needs to be rewritten, simp will be rewritten, linarith might be rewritten

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 22:47):

Should mathlib porting guidelines make a firm statement about set_option autoBoundImplicitLocal false?

view this post on Zulip Mario Carneiro (Jan 06 2021 at 22:48):

What's it mean?

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 22:49):

Consider the following: https://gist.github.com/shingtaklam1324/7451d7e329aa32efd42dd49d784ac8a5#file-algebra_groups_defs-lean-L15

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 22:49):

The u is coming from the fact that it is a lowercase letter, and can be inferred, so it is.

view this post on Zulip Mario Carneiro (Jan 06 2021 at 22:49):

I would say use it freely

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 22:49):

As remarked on here https://leanprover.github.io/lean4/doc/autobound.html?highlight=lower#auto-bound-implict-arguments

view this post on Zulip Mario Carneiro (Jan 06 2021 at 22:50):

If it's possible, I want to bring back Sort* via notation

view this post on Zulip Mario Carneiro (Jan 06 2021 at 22:51):

I think, as long as it's still basically making the right guesses, we should use Sort* or Type* wherever possible, because it makes universe errors less likely

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 22:51):

The bottom snippet in https://leanprover.github.io/lean4/doc/typeobjs.html?highlight=type%20_#types-as-objects is about Type* or Sort*

view this post on Zulip Mario Carneiro (Jan 06 2021 at 22:51):

Right, we're going to need a mathlib prelude anyway and this should go in it

view this post on Zulip Mario Carneiro (Jan 06 2021 at 22:53):

For times when it's necessary to use explicit universes, it's marginally more convenient to use implicit universe arguments than universes u v which is mostly noise

view this post on Zulip Kenny Lau (Jan 07 2021 at 12:22):

https://github.com/kckennylau/mathlib4/blob/master/src/logic/basic.lean

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 12:22):

Is that the official mathlib port repo? :D

view this post on Zulip Kenny Lau (Jan 07 2021 at 12:22):

it’s my unofficial mathlib port repo

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 12:23):

You'd better document your instances or the linter will complain

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 12:23):

In fact @Jesse Michael Han was telling me that we should document all theorems too, because then AI will be able to learn better about mathematical natural language

view this post on Zulip Eric Wieser (Jan 07 2021 at 12:31):

Maybe then we can train gpt to insert a comment explaining in natural language why it rewrote add_comm repeatedly

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 12:31):

"Because it's there"

view this post on Zulip Eric Wieser (Jan 07 2021 at 12:32):

More seriously though, that knowledge would definitely help build a more powerful method for searching theorems in the docs

view this post on Zulip Jesse Michael Han (Jan 07 2021 at 20:43):

Kevin Buzzard said:

In fact Jesse Michael Han was telling me that we should document all theorems too, because then AI will be able to learn better about mathematical natural language

yes, this would be extremely useful as training data for informal-to-formal machine translation

view this post on Zulip Eric Wieser (Jan 07 2021 at 20:56):

Perhaps vice versa too, given the discussion in the teaching panel about transitioning to paper from lean

view this post on Zulip Mohamed Al-Fahim (Jan 07 2021 at 23:41):

(deleted)

view this post on Zulip Alena Gusakov (Jan 08 2021 at 14:55):

I wonder if there are some areas of interest to mathlib that are not well represented in mathlib so far (and so have few serious dependecies).

graph theory and combinatorics!

view this post on Zulip Kenny Lau (Jan 08 2021 at 14:57):

@Alena Gusakov so are you going to work on graph theory in Lean 4

view this post on Zulip Alena Gusakov (Jan 08 2021 at 14:57):

I might

view this post on Zulip Alena Gusakov (Jan 08 2021 at 14:58):

I've just barely started wrapping my head around how Lean 3 works but it might be worth it for me to start experimenting w/ Lean 4 since we're planning to port anyway

view this post on Zulip Kenny Lau (Jan 08 2021 at 15:01):

let's go

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 04:48):

@Huỳnh Trần Khanh thank you. i am interested in experimenting with some category theory stuff in lean. is anything available yet for lean4? how long would you expect for mathlib to be upgraded for lean4? as someone who has never uesd lean before, would you suggest i stick to lean3 for now or to try to port myself the relevant bits from mathlib to lean4?

view this post on Zulip Huỳnh Trần Khanh (Feb 02 2021 at 05:06):

@Nasos Evangelou-Oost I'd say stick with Lean 3 for now. Lean 4 is still unstable.

view this post on Zulip Huỳnh Trần Khanh (Feb 02 2021 at 05:08):

There was a recent soundness bug. Already fixed, but who knows if there are still other bugs lurking somewhere.

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:08):

more importantly, it doesn't have many of the features of lean 3 yet, only the ability to eventually write them. This is going to take a while

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 05:15):

@Huỳnh Trần Khanh i see. actually what i'm more interested is in computational category theory and general purpose programming. i recently was surprised to learn that lean4 is actually quite capable of this. i'm currently working on a project in F# but the lack of dependent types is limiting. i also considered idris2 as a general-purpose dependently typed language but it is in prerelease and its development seems slow (idris 1 seems too slow to be able to do anything useful).

view this post on Zulip SnowFox (Mar 16 2021 at 21:09):

Is there a roadmap until port : Lean3 -> Lean4 port mathlib?

view this post on Zulip Sayantan Majumdar (Mar 27 2021 at 22:15):

lean4 seems significantly different. Does this mean mathlib has to be written again?

view this post on Zulip Kevin Buzzard (Mar 27 2021 at 22:48):

Lean 4 is very similar to lean 3, but sufficiently different to make porting the maths library a nontrivial problem. Right now we're letting the experts think about this but it's still early days.


Last updated: May 07 2021 at 13:21 UTC