Lean 3.4

Stream: general

[Patrick Massot]

Does this monadic merge get us closer to Lean 3.4? Or is there still WIP on the type_context/name refactorings blocking?

[Sebastian Ullrich]

Lean 3.4 should be released in the next few days

[Kevin Buzzard]

I am seriously considering writing my undergraduate course materials for Oct-Dec 2018 in Lean 3.4 stable. Are there any other concrete plans for more stable releases in the 3.x line, or is the plan to make 3.4 and then just do bug fixes whilst concentrating on 4?

[Sebastian Ullrich]

3.x will be in maintenance mode, I wouldn't expect anything other than bugfixes, and perhaps minor features wanted by MSFT people :)

[Kevin Buzzard]

what is MSFT?

[Sebastian Ullrich]

Microsoft

[Kevin Buzzard]

Aah. I had guessed that the M stood for Microsoft but I wasn't sure about the other letters :-)

[Mario Carneiro]

it's the stock code

[Jakob von Raumer]

I've seen the Lean 4 design notes, but is there any list of what parts of existing Lean 3 code are going to break?

[Mario Carneiro]

It's hard to say at this point, but generally any major change to an area will break stuff that relies on details of how it works

[Sebastian Ullrich]

There aren't many APIs that expose details of the current parser or esp. the current code generator. The biggest chance of breakage should come from things that we know we want to rewrite anyway and don't want to maintain until then (SMT mode, algebraic hierarchy, ...).

[Peter Jipsen]

I am interested in the Lean 4 design notes. Are they public? In particular, I would like to implement more of the algebraic hierarchy in Lean, so information on how that will change would be useful.

[Simon Hudon]

It used to be available here: https://github.com/leanprover/lean/blob/80d68a7605e4bb478d789ad121303745663fb192/tmp/lean4.md (this is an old commit) but it seems to have been moved to Google Docs and I'm not sure if Leo is sharing that document

[Mario Carneiro]

Leo has gone to ground (even more than before). I don't know if he will pop up again, but I doubt it. Sebastian is the only one privy to those plans now AFAIK

[Patrick Massot]

It looks like a significant part of https://leanprover.github.io/about/ is now outdated

[Simon Hudon]

The last release is out!

[Simon Hudon]

I noticed:

Lean 4
------

We are currently developing Lean 4 in a new (private) repository.
The source code will be moved here when Lean 4 is ready.
Users should not expect Lean 4 will be backward compatible with Lean 3.

In the release notes. I wonder why Lean 4 is made in private. Maybe so the users won't flood Leo's mailbox with requests.

[Leonardo de Moura]

Yes. I want to work in peace.

[Simon Hudon]

Alright! I'm looking forward to seeing what you come up with

[Leonardo de Moura]

Jakob, I added a few notes for the Lean 4 goals. It will not be backward compatible, like Lean3 was not compatible with Lean2.

[Leonardo de Moura]

It looks like a significant part of https://leanprover.github.io/about/ is now outdated

Why?

[Patrick Massot]

At the time I wrote that message, the webpage still said: "It is a collaborative open source project, hosted on GitHub. Contributions to the
code base and library are welcome". The second sentence has since been removed. The first one is still somehow misleading since the current development and discussion happens in a private branch, but it's true the source code of the current version is available. Although I felt some frustration about not seeing Lean 4 work in a public branch, my main point was really that the contributions sentence could only lead to frustration for everybody (potential contributors and you).

The Lean 4 frustration part was 100% curiosity frustration, nothing serious at all. I have absolutely zero expertise in theorem prover coding, and couldn't contribute anything to Lean 4 (except maybe documentation). So I'm perfectly fine with not seeing what you are doing. I'm a mathematician who thinks proof assistant should become important for mathematicians. And I love that Lean seems to be much easier to learn and much more usable for us than Coq. This is already true of Lean 3. So I try to learn, and write very small scale experimentation.

By the way, thank you very much for releasing Lean 3.4. It will make it much easier to point out to colleagues who also want to try. Are you interested in PR on the reference manual? Maybe this is worth the effort if other people than core devs do it, because I guess Lean 3.4 will stay the current version for quite some time, and your time certainly better spent on writing Lean 4 than documenting Lean 3.4.

[Leonardo de Moura]

I will remove the word "collaborative". The project is still open source. Keep in mind that being "open source" doesn't imply that we have to make the development and discussions public. I tried it, and it doesn't work for me.
Regarding "curiosity frustration", I understand it, but the open development/discussion model does not work for me. As I told Mario a few days ago, Lean is open source, he (or any other person) can fork the project and manage it in a different way or use a different development model.
Regarding PR's for the reference manual, they are fine, but whoever is working on it must keep in mind that Lean 4 may not be backward compatible with Lean 3.

[Simon Hudon]

Out of curiosity, was it any less frustrating to have Z3 open source?

[Leonardo de Moura]

Z3 was much easier. First, when we released the source code, Z3 was already a mature system being used in production at Microsoft and in many research projects. Second, Z3's interface is much simpler, and it is not used by end users. Z3 users are tool builders / software developers. Finally, I never felt harassed by Z3 users.

[Patrick Massot]

Although I wasn't there at that time, I understand very well that you tried a more public development and it didn't work. Actually it's not surprising that such a complex and subtle project needs a very small team. It's not like everyone could contribute a tiny piece of Lean core. Also if I understand correctly, many goals of Lean 4 will make all this easier. More interface exposed, less maths in core lib, more extensible parser... all this sounds like people will be able to use Lean in more complicated ways without bothering you.

[Patrick Massot]

And again I want to insist that all users I see are already very happy about the current Lean

[Patrick Massot]

In particular I think it makes sense that people (not you) write documentation for Lean 3.4 so that we can still experiment with Lean while you peacefully work on the next version.

[Kevin Buzzard]

Thank you Leo for contributing to this conversation and in particular for making it clear that Lean 4 will make no attempt to be backward compatible with Lean 3.4. I think that it is essentially inevitable that when Lean 4 appears, people will attempt to port mathlib over to it. It should be an interesting experience. As I said to Sebastian recently, basically I write mathematics in Lean 3.4 because I am a mathematician in my late 40s and I had no idea really that research level mathematics could be written in this way. I feel like I've been waiting for this language all my life and I find writing mathematics in Lean really good fun. I am currently attempting to write the basic mathematical theory of schemes in Lean 3.4 and I am learning so much about dependent type theory and how it relates to mathematics. If the whole thing doesn't work at all in Lean 4 then I will still have learnt so much.

[Kevin Buzzard]

It will be a while before the global mathematical community starts seeing these tools as normal, so I don't think there is any need to worry about people continuing to write mathematics in Lean 3.4. The way I see it, currently we need mathematicians to engage with this sort of software in general and it will take time for the user base to grow. From this point of view, backwards compatibility is not really a problem. The problem is that Coq has been around for decades and mathematicians still don't use it.

[Patrick Massot]

I think we can at least assume Lean 4 will be based on some kind of dependent type theory. So clearly we will have learned useful stuff while using Lean 3.

[Kevin Buzzard]

Indeed.

[Patrick Massot]

By the way Kevin, I met someone else who seems excited by proof assisants: Eleonora Di Nezza, who seems to know you.

[Simon Hudon]

I'm sorry your experience has been so negative. I'm glad that you're still moving forward with the project as I greatly appreciate your vision. I routinely find new versions coming out with features I didn't know I wanted. Or at time, when wishing for feature X, I find feature Y coming out which is much better than what I was hoping for.

[Leonardo de Moura]

Patrick and Kevin, yes Lean 4 will still be based on dependent type theory. The only significant change to the kernel is support for nested inductive datatypes.

[Kenny Lau]

@Leonardo de Moura will there be coinduction? :D

[Kenny Lau]

and what kind of change will there be to the nested inductive datatypes?

[Patrick Massot]

Kenny, don't start harassing Leo!

[Leonardo de Moura]

@Kenny Lau No, we are not considering coinduction for Lean 4. We will only consider it after we have "succeeded". That is, we have managed to develop real verified software using Lean. The coinductive predicates developed by Johannes are sufficient for achieving this goal.

[Kevin Buzzard]

Kenny -- do we really need coinduction to do mathematics? I have not yet run into any mathematics which Lean in its current state could not handle, and you know as well as I do how "deep" the scheme code is coming out.

[Leonardo de Moura]

@Kenny Lau Right now, nested inductive datatypes are compiled into a more basic version accepted by the kernel. If you define one, and use the #print command to inspect it, you can see how they are encoded. This compilation process creates several technical problems.

[Kevin Buzzard]

All that happens as far as I am concerned is that I have to think slightly more deeply and carefully about the mathematics than I did before.

[Kevin Buzzard]

Random Lean 3.4 questions: will there be a mathlib 3.4 branch? Will someone update the lean web editor to 3.4 + mathlib 3.4? Will PRs for the Lean docs to upgrade them to 3.4 be welcome?

[Mario Carneiro]

Yes, as soon as the nightly comes out

[Mario Carneiro]

Well, there won't be a 3.4 branch, there will be a master branch that is keyed to lean master like normal, but lean master is going to be relatively stationary for the next while as Leo works on lean 4 in private

[Mario Carneiro]

But we can tag a version of mathlib that matches the 3.4 release

[Patrick Massot]

Kevin, I asked your last question to Leo yesterday, he answered: "Regarding PR's for the reference manual, they are fine, but whoever is working on it must keep in mind that Lean 4 may not be backward compatible with Lean 3." https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/Lean.203.2E4/near/125203831

[Patrick Massot]

Also, Jeremy wrote that he will work on updating TPIL on Thursday and Friday

[Sean Leather]

I just want to add my gratitude to Leo for a very enjoyable experience proving theorems with Lean. I have tried many other proof assistants (Agda, Coq, Idris, and Isabelle/HOL), and I have not found one that was as fast or as pleasant to use as Lean. Lean 3 was a definite improvement over Lean 2, and I look forward to Lean 4 being an improvement over Lean 3. (I only hope the migration process is not as painful as the previous one.)

I am sorry to hear about the implied harassment by Lean users that appeared due to the open development model. I have not seen any obvious signs of harassment on any of the public forums in which I have participated. Perhaps I missed it, or perhaps it happened in other venues. Most of the communication I've seen was rather respectable and polite.

I hope that I have not, in any way, contributed to this harassment or the perception thereof. I reviewed all of my lean-user forum emails and GitHub issue comments, and I don't think I said anything that was mean or derogatory. I try to be clear, respectful, and constructive. If I unwittingly failed to do this, I sincerely apologize.

I admit to being a proponent of an open development model for open-source software, and I have previously voiced concerns and recommendations regarding that with Lean. On the one hand, it fills me with regret that Lean development will happen in private. I feel that working with a community (such as the wonderful one we have here on Zulip) is a fruitful way to produce good software. But, on the other hand, I can accept that, if Lean development is to continue and progress is to be made, Leo must operate in a way that works for him, since, after all, he is the primary developer.

And, lastly, thanks, Leo, for coming on here to explain things. I know the community appreciates being informed, as do I.