Hello World!

Stream: new members

[Tor-Haakon Gjone]

Hi everyone. My name is Tor, and I just finished the tutorial and would like to try to contribute something.
I'm a third semester master studying at the University of Bonn.
I've been browsing the math-lib docs trying to find something I might contribute. I noticed that geometry seems quite sparse so I was thinking of implementing some basic Riemannian geometry.

[Jireh Loreaux]

"some basic Riemannian geometry" is likely a significant amount of work, but likely @Heather Macbeth, @Oliver Nash and @Patrick Massot are among the people you want to talk to about it.

[Patrick Massot]

Yes, this is a very ambitious first goal, because using manifolds in mathlib is really tricky.

[Patrick Massot]

There are more accessible targets listed at https://leanprover-community.github.io/undergrad_todo.html. Please discuss here before tackling one, if only to make sure nobody is working on it.

[Kevin Buzzard]

An Imperial undergraduate at Xena yesterday was also talking about starting on Riemannian geometry. Is it really so impossible to start on this?

[Heather Macbeth]

It is not even possible yet to define a Riemannian metric yet, though it's within reach -- probably in a month or two, once ongoing work like #17611 and #17680, and follow-ups like smooth bundles of endomorphisms, are defined. Of course, I already have strong opinions about how it should be done (and I'm sure Patrick, Oliver, Sebastien, etc. do too).

[Heather Macbeth]

If someone wants an accessible project involving manifolds, there are plenty of other options. One that I have proposed elsewhere on Zulip is to define the groupoid of orientation-preserving maps, and then use this to define oriented manifolds.

[Kevin Buzzard]

Thanks -- I'll pass this on!

[Tor-Haakon Gjone]

Thanks for the reply. I'll have a look at the todo list :D

[Heather Macbeth]

What area is your masters in, Tor-Haakon?

[Paul Lezeau]

Heather Macbeth said:

If someone wants an accessible project involving manifolds, there are plenty of other options. One that I have proposed elsewhere on Zulip is to define the groupoid of orientation-preserving maps, and then use this to define oriented manifolds.

Here's the link to the Zulip conversation I think you're referring to : https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Symplectic.20geometry/near/267353636

[Paul Lezeau]

These mini projects are still on my todo list, but I've gotten caught up in other stuff so feel free to take these on if you want @Tor-Haakon Gjone ;)

[Tor-Haakon Gjone]

Heather Macbeth said:

What area is your masters in, Tor-Haakon?

I guess my master is in geometry, though I've done almost as much algebra and topology so far.

[Tor-Haakon Gjone]

@Paul Lezeau Cool. I'll give the oriented manifolds a try :D

[Paul Lezeau]

Awesome, good luck ! ;)