Stream: Miscellaneous

Topic: Lean Together 2021


view this post on Zulip Bas Spitters (Jan 03 2021 at 19:02):

BTW. Lean together starts tomorrow:
https://leanprover-community.github.io/lt2021/schedule.html

view this post on Zulip Karl Palmskog (Jan 04 2021 at 10:05):

apparently there is some graph theory formalization going on in the Lean world:

ping @Christian Doczkal who might be interested in comparing formalization notes (at least I would be interested in any Lean-vs.-Coq project/ecosystem comparisons)

view this post on Zulip Rob Lewis (Jan 04 2021 at 11:58):

Oh, how nice, I logged in here to post this and there's already a topic :smile: Things will start in a few hours. There are a handful of Coq/Agda/MetaMath talks mixed into the program.

Here are the meeting details -- please don't post these more publicly than this though! If you're planning to stick around a while, we'd appreciate it if you registered, just so we can have a vaguely accurate count.

Main workshop on Zoom:
https://tinyurl.com/ybvxnwjg (tinyurl to prevent bot identification)
Meeting ID: 985 5254 7841
Passcode: induction

Social time on Wonder:
https://www.wonder.me/r?id=f3cc3041-0c16-42df-a556-ae77b316c113

view this post on Zulip Karl Palmskog (Jan 04 2021 at 12:33):

@Rob Lewis are there any abstracts of the talks? Sometimes hard to decide to attend just based on title.

view this post on Zulip Rob Lewis (Jan 04 2021 at 12:36):

Between the late organization and the holidays, it was hard enough to extract titles from all the speakers, heh. Afraid this is all we have.

view this post on Zulip Karl Palmskog (Jan 04 2021 at 12:39):

OK I see.

view this post on Zulip Théo Zimmermann (Jan 04 2021 at 14:56):

I'm looking forward to the Lean 4 and mathlib talks.

view this post on Zulip Karl Palmskog (Jan 04 2021 at 18:35):

it seems everyone arrives at the Nix / package manager dichotomy...

view this post on Zulip Théo Zimmermann (Jan 04 2021 at 18:46):

With unification hints back and such a use of Nix, I wondered if they didn't do it only to get @Cyril Cohen to switch to Lean :stuck_out_tongue_wink:

view this post on Zulip Bas Spitters (Jan 04 2021 at 19:20):

Did @Cyril Cohen switch to Lean :scream:

view this post on Zulip Karl Palmskog (Jan 04 2021 at 19:25):

not yet I believe, but Leo de Moura and Sebastian Ullrich gave him some strong reasons to in the Lean workshop

view this post on Zulip Karl Palmskog (Jan 04 2021 at 19:26):

all paths apparently lead to Nix and canonical structures

view this post on Zulip Bas Spitters (Jan 04 2021 at 19:27):

Are the unification hints just the lean type classes, or is there a new paper?

view this post on Zulip Karl Palmskog (Jan 04 2021 at 19:28):

I don't think they will write a paper on them specifically, but unification hints (standalone and not via type classes) are apparently a part of the new release: https://github.com/leanprover/lean4/releases/tag/v4.0.0-m1

view this post on Zulip Cyril Cohen (Jan 04 2021 at 21:09):

"Switching" to Lean is a big word, but I will definitely try it out...

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

For those of you who weren't following live, recordings of yesterday's talks are up on YouTube. We'll update that playlist at the end of each workshop day.

view this post on Zulip Karl Palmskog (Jan 05 2021 at 09:56):

I think we need to screenshot Leo's archetypes somewhere (or copy out from slides if available)...

view this post on Zulip Enrico Tassi (Jan 05 2021 at 09:57):

If only zulip had badges

view this post on Zulip Karl Palmskog (Jan 05 2021 at 09:59):

view this post on Zulip Karl Palmskog (Jan 05 2021 at 10:06):

choose your fighter collaborator!

view this post on Zulip Théo Zimmermann (Jan 05 2021 at 10:06):

It's sad that it was Leo's most common experience with external contributors to Lean. Maybe that was because Lean got too popular too fast? In any case, we had a better experience with external contributors to Coq.


Last updated: Aug 19 2022 at 19:03 UTC