Evan Bailey (self-introduction)

Stream: new members

[Evan Bailey]

Hi everyone!

My name is Evan Bailey. I recently completed my undergrad with a dual major in Math and CS. I have read/solved most of Mathematics in Lean and I have really enjoyed using Lean so far!

I would love the opportunity to contribute to Mathlib! Given my background, I would probably be most helpful in the (very broad) areas of computability/complexity theory, graph theory, lattice combinatorics, decision procedures, or metaprogramming. If anyone knows about specific topics that I could help with, especially in those areas, please let me know!

Additionally, I have some ideas about how to formalize the notion of the arclength of a curve in a PseudoEMetricSpace and some related topics (rectifiable curves, length spaces, geodesic curves, geodesic spaces, unique geodesic spaces, the Hopf-Rinow theorem, etc.). This would probably consist of two new files - Topology/EMetricSpace/Length.lean and Topology/MetricSpace/Length.lean - and some minor changes to other files. As far as I can tell, these do not yet exist in Mathlib.

I would love to hear feedback on this idea and am happy to share more details. If this makes sense as a feature, I was wondering if I could have access to a non-master branch to implement this (my GitHub username is E-M-Bailey).

[Yaël Dillies]

Hey! I have worked extensively on combinatorics in mathlib, so I can give you some pointers there

[Yaël Dillies]

Eg are you interesting in communication complexity? I have a half-finished project which is looking for someone to take over it. It is about the Chandra-Furst-Lipton paper on deterministic complexity in the Number On the Forehead model.

[Yaël Dillies]

Evan Bailey said:

Additionally, I have some ideas about how to formalize the notion of the arclength of a curve in a PseudoEMetricSpace and some related topics (rectifiable curves, length spaces, geodesic curves, geodesic spaces, unique geodesic spaces, the Hopf-Rinow theorem, etc.).

Please try :smile:

[Michael Rothgang]

Yaël Dillies said:

Evan Bailey said:

Additionally, I have some ideas about how to formalize the notion of the arclength of a curve in a PseudoEMetricSpace and some related topics (rectifiable curves, length spaces, geodesic curves, geodesic spaces, unique geodesic spaces, the Hopf-Rinow theorem, etc.).

Please try :smile:

Yes, please! I believe @Ben Eltschig had some thoughts about this (but isn't actively working on this) --- just in case some exchange of ideas is useful :-)

[Ben Eltschig]

I only toyed around with lengths of paths in Riemannian manifolds a bit last year - I didn't get all that far though, in part because I didn't understand mathlib nearly as well back then as I do now. I do think that it probably makes sense to formalise more general notions like length spaces first, so I'm curious to see what comes out of it if you give that a try.

[Evan Bailey]

Yaël Dillies said:

Eg are you interesting in communication complexity? I have a half-finished project which is looking for someone to take over it. It is about the Chandra-Furst-Lipton paper on deterministic complexity in the Number On the Forehead model.

Thanks for the suggestion! I do find communication complexity to be interesting. Do you have a link I could look at to learn more about the project?

[Yaël Dillies]

You can read everything we have and want to have at yaeldillies.github.io/ChandraFurstLipton

[Michael Bucko]

Yaël Dillies schrieb:

You can read everything we have and want to have at yaeldillies.github.io/ChandraFurstLipton

Thank you for sharing this! It's very informative!
Bildschirmfoto 2024-10-12 um 23.23.13.png