Stream: Miscellaneous

Topic: Lean Together 2021

Bas Spitters (Jan 03 2021 at 19:02):

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

Karl Palmskog (Jan 04 2021 at 10:05):

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

• Thursday, January 7, 4:00pm CET, "Formalizing Hall’s Marriage Theorem"

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)

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

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.

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.

Karl Palmskog (Jan 04 2021 at 12:39):

OK I see.

Théo Zimmermann (Jan 04 2021 at 14:56):

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

Karl Palmskog (Jan 04 2021 at 18:35):

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

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:

Bas Spitters (Jan 04 2021 at 19:20):

Did @Cyril Cohen switch to Lean :scream:

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

Karl Palmskog (Jan 04 2021 at 19:26):

all paths apparently lead to Nix and canonical structures

Bas Spitters (Jan 04 2021 at 19:27):

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

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

Cyril Cohen (Jan 04 2021 at 21:09):

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

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.

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)...

Enrico Tassi (Jan 05 2021 at 09:57):

If only zulip had badges

Karl Palmskog (Jan 05 2021 at 09:59):

• "The inquisitor" - asks a bunch of questions but doesn't do anything
• "The dreamer" - has big ideas, but never delivers anything
• "The socializer" - wants to have fun, tell jokes, discuss wild ideas
• "The clueless" - requires a lot of attention, and can't figure out anything
• "The over confident" - knows it all, although never built anything
  https://youtu.be/UeGvhfW1v9M?t=4182
  

Karl Palmskog (Jan 05 2021 at 10:06):

choose your fighter collaborator!

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: Oct 13 2024 at 01:02 UTC