Zulip Chat Archive

my background: used to me a mathematician (rep theory, higher categories, and applications to low dim topology). now I work in tech, mostly ML. there's nothing in particular I want to prove! just exploring curiously. once I learn more, I'd be interested in contributing to formalization projects, but I don't know much about what's going on in the lean community

Matthew Ballard (Apr 13 2022 at 19:58):

Lean 3 currently has a developed pure mathematics library - mathlib.

Bryan Gin-ge Chen (Apr 13 2022 at 19:58):

Until mathlib has been ported over to Lean 4 (which should hopefully happen within the next year or so), I'd recommend starting with Lean 3. The community website has a bunch of learning resources here: https://leanprover-community.github.io/learn.html

Matthew Ballard (Apr 13 2022 at 19:59):

Unless you want to roll your own "basic" theorems and proofs, then I would suggest starting there

Alex Ellis (Apr 13 2022 at 20:00):

thanks! yes, matlib is what I've been playing with so far. good to know there are plans to port it to lean4. I'm curious—what's the reason lean is choosing to have non-backwards-compatible releases?

Matthew Ballard (Apr 13 2022 at 20:00):

Greater functionality

Matthew Ballard (Apr 13 2022 at 20:02):

Unlike most programming languages where the terrain is pretty well-trodden, a lot is learned here with trial and error.

Bryan Gin-ge Chen (Apr 13 2022 at 20:06):

As the Lean 4 FAQ puts it "Lean is under heavy development, and we are constantly trying new ideas and tweaking the system. It is a research project and not a product."

Matthew Ballard (Apr 13 2022 at 20:10):

It also has a section on significant changes from Lean 3 to Lean 4.

Eric Wieser (Apr 13 2022 at 20:10):

The best time to make a backwards incompatible release is when your userbase is small, and your core users (here mathlib contributors) are willing to put up with the incompatibility. Lean has the luxury of being in that position unlike many other languages.

Matthew Ballard (Apr 13 2022 at 20:12):

Personally, I think the benefits derived from the breaking changes will significantly outweigh the hassles. For example, program extraction + proofs is :fire: for me.

Matthew Ballard (Apr 13 2022 at 20:13):

I think the majority of the current user base feels similarly generally.

Eric Wieser (Apr 13 2022 at 20:16):

It's worth remembering that mathlib is already very backwards incompatible anyway

Notification Bot (Apr 13 2022 at 20:19):

15 messages were moved here from #general > Tips and tricks by Rob Lewis.

Arthur Paulino (Apr 13 2022 at 20:20):

And from a software engineering perspective, the freedom to go backwards incompatible comes with the freedom to make bold improvements, such as completely revamping the metaprogramming infra

Yaël Dillies (Apr 13 2022 at 20:58):

Some people do come on Zulip every now and then to grumble about a lemma that doesn't exist anymore, but fixing it is usually a matter of minutes.

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib