Zulip Chat Archive

Hello! I'm a Maths & Computer Science undergrad at the University of St Andrews & I will be writing my final year project in Lean. I'd love to get chatting with some of you to share ideas as I'm quite new to lean!

Kevin Buzzard (Sep 20 2022 at 15:14):

Who's supervising you and do you have an idea of topic?

Will Midwood (Sep 21 2022 at 10:04):

Dr. Louis Theran, and no not as of yet, still in early talks about a topic. I would love to contribute to mathlib though, so the Containers theorem about hypergraphs is one Idea we've had so far.

Will Midwood (Sep 21 2022 at 13:18):

Oh and Dr. Susmit Sarkar, as this is a joint project between the Schools of Maths and Computer Science.

Bryan Gin-ge Chen (Sep 21 2022 at 14:56):

Welcome! Please give my regards to Louis. Just based on skimming the wikipedia page on the container method I suspect @Yaël Dillies would be able to give you some helpful pointers.

Mauricio Collares (Sep 21 2022 at 15:39):

Although hypergraph containers are cool, I think it makes sense to go for graph containers (as in, say, https://arxiv.org/abs/1412.0940) first

Mauricio Collares (Sep 21 2022 at 15:41):

It relies on less prerequisites for formalization, the proof is shorter, it has many applications and tends to be more efficient when applicable (that is, it is not completely subsumed by hypergraph containers)

Yaël Dillies (Sep 22 2022 at 09:33):

Sorry, I'm afraid I don't know anything about containers!

Andrés Goens (Sep 29 2022 at 11:42):

Will Midwood said:

Oh and Dr. Susmit Sarkar, as this is a joint project between the Schools of Maths and Computer Science.

I happen to be working on a Lean-based project with him, but it's not really related to Mathlib, it's more of a CS topic (about properties of memory consistency models). Happy to chat about that too if the topic is very open and you're interested :) @Will Midwood

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib