Zulip Chat Archive

Stream: Geographic locality

Topic: Dublin, Ireland

Oliver Nash (Feb 28 2020 at 12:49):

Top of the morning to you. :shamrock:️

I’d love to talk to anyone interested in mathlib here in Dublin.

Jose Balado (Apr 12 2020 at 13:55):

Hi, I am in Dublin also, but my knowledge or Mathematical Logic and Lean is just pretty basic. I played a little bit with Lean some months ago translating basic Propositional and First Order Logic to Lean.

Dan Stanescu (Apr 12 2020 at 14:09):

(deleted)

Oliver Nash (Apr 13 2020 at 11:07):

That's marvellous, I'm not on my own here in Dublin. I guess with the :locked: :down: geographic location doesn't really matter but even still, I'd love to hear if you are involved in any Lean / Mathlib work.

Oliver Nash (Apr 13 2020 at 11:10):

For my part, I am extremely interested in the Mathlib project, so I try to contribute bits and pieces to that when I have time.

Jose Balado (Apr 13 2020 at 19:39):

Hi Oliver, thank for your message.
Sadly I am not involved in Mathlib, I wish, but my knowledge is too basic. I am just learning some basic Type Theory and Lambda Calculus.

Scott Olson (Jun 26 2020 at 10:40):

Hello! I've just moved from Canada to Dublin a few months ago (pretty much just before lockdown).

I'm a programmer and I've been interested in dependent types for about a decade, learning Coq, Agda, and others on and off, finally landing on Lean/VSCode as it has the best UX situation in the whole field as far as I can tell. I've used mostly used Lean+mathlib to teach myself interesting math (mostly on the CS/type theory side) by implementing it, which makes it feel a lot more concrete to me. For example, regular languages/expressions and container theory.

Scott Olson (Jun 26 2020 at 10:44):

I'd also say I've learned quite a bit just by studying mathlib's definitions, such as finite types, finite sets, multisets, quotients, and more. I find that the constructive type theory approach illuminates a lot of topics better for me than typically informal set theory approaches.

Oliver Nash (Jun 26 2020 at 14:26):

Hello and welcome @Scott Olson, both to Zulip and to Dublin. You have far more experience than I do so it's interesting to hear you say that you find Lean+VSCode the best UX. I can only compare with Coq+CoqIDE which was ... less pleasant.

Oliver Nash (Jun 26 2020 at 14:30):

I also find that reading Mathlib has greatly improved my expertise in Lean, such as it is. Making minor contributions when time allows, helps a lot too.

Scott Olson (Jun 26 2020 at 14:42):

My hands-on experience is basically limited to Coq+CoqIDE, Agda+Emacs, and Lean+VSCode, but the first is painfully unmodern (both the language and the software) and while the second can be made nice, it's not exactly for beginners, and you'll have to know how to deal with Emacs. By comparison, when I tried Lean for the first time I was shocked how low-friction it was to get started.

Oliver Nash (Jun 26 2020 at 14:59):

Having the community here also helps a lot. I remember being very, very confused about many things in Coq about a year ago when I was trying to get started in this stuff. E.g., https://stackoverflow.com/questions/55599660/why-does-coq-object-to-the-following-pairusualdecidabletypefull-module-type

Kevin Buzzard (Jun 26 2020 at 15:07):

I remember thinking "wooah, mathoverflow, that's so much better than sci.math.research for making progress" but stackoverflow now looks like a very inefficient way to solve technical questions like that.

Johan Commelin (Jun 26 2020 at 15:09):

I've seriously been contemplating whether I should start algebraic-geometry.zulipchat.com

Jalex Stark (Jun 26 2020 at 15:13):

there's demand, i think. a bunch of people signed up for this and some of them would hang out in your server and ask questions

Jalex Stark (Jun 26 2020 at 15:14):

this place succeeds on the back of coordinating PRs to mathlib

Jalex Stark (Jun 26 2020 at 15:15):

an algebraic geometry server with regulars who are talking about their active PRs to the stacks project would probably succeed

Rob Lewis (Jun 26 2020 at 15:16):

The Zulip team has been talking about publicly visible/crawlable streams for years, since before I wrote the stupid archive script, and there's still no progress as far as I know. It's a real blocker to a lot of cases where otherwise Zulip would be great. So much information hidden because search engines can't find it properly and people need to log in to see it.

Scott Olson (Jun 26 2020 at 15:18):

Zulip seems like it fits into a good place on the synchronous/asynchronous chat spectrum for communities like this. It's a bit smoother than a forum or a formal question/answer site, but topics have a bit more permanence than instant messaging.

Kevin Buzzard (Jun 26 2020 at 15:19):

It is a shame about visibility. I think that Lean visibility online in general is poor because the word means so many other things (I bet dedukti don't have that problem) and because search engines like to send you to the dead MS pages.

Kevin Buzzard (Jun 26 2020 at 15:20):

searching for mathlib on the other hand works remarkably well

Scott Olson (Jun 26 2020 at 15:20):

yeah, I often have to change my searches to "leanprover"

Rob Lewis (Jun 26 2020 at 15:21):

Have you ever searched mathlib on Twitter? There's a lot of stuff like this, apparently madlibs but for math or something. https://twitter.com/NWhiteSchools/status/1197680436635471873

Patrick Massot (Jun 26 2020 at 15:32):

It seems the global proof assistant community has really serious difficulties coming up with names.

Johan Commelin (Jun 26 2020 at 17:07):

I like serious. If I ever write my own theorem prover, I'll call it serious.

Emil Sköldberg (Oct 16 2020 at 15:07):

I'm in Galway and not in Dublin, but still it's nice to see that there are others in Ireland interested in mathlib. I've only very recently started to look at it, and I hope I get some more time later in the semester to experiment with it.

Last updated: Dec 20 2023 at 11:08 UTC