BTW. Lean together starts tomorrow:
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)
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
Social time on Wonder:
@Rob Lewis are there any abstracts of the talks? Sometimes hard to decide to attend just based on title.
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.
OK I see.
I'm looking forward to the Lean 4 and mathlib talks.
it seems everyone arrives at the Nix / package manager dichotomy...
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:
Did @Cyril Cohen switch to Lean :scream:
not yet I believe, but Leo de Moura and Sebastian Ullrich gave him some strong reasons to in the Lean workshop
all paths apparently lead to Nix and canonical structures
Are the unification hints just the lean type classes, or is there a new paper?
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
"Switching" to Lean is a big word, but I will definitely try it out...
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.
I think we need to screenshot Leo's archetypes somewhere (or copy out from slides if available)...
If only zulip had badges
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: Dec 01 2023 at 06:01 UTC