Amsterdam, NL and soon Reykjavik, IS

Stream: Geographic locality

[Gunnar Þór Magnússon]

Hello! I used to do complex differential geometry (compact Kahler manifolds with applications to algebraic geometry) before becoming a developer. I'm in Amsterdam until the summer when we plan to move back home to Iceland. I'm interested in playing around with Lean in general and formalizing things related to complex geometry in particular (though I see it may be quite a while before mathlib gets there).

[Johan Commelin]

Well, if #10000 is merged, then complex analysis kicks of seriously. And I know that @Sebastien Gouezel is aiming for differential forms and de Rham cohomology. So maybe the Kähler condition isn't actually that far off in the future.

[Gunnar Þór Magnússon]

I imagine there's a roadmap for getting to complex manifolds and differential geometry. If I can help in any way I'd be happy to do so, like with complex analysis or differential forms or manifolds or analytic sheaves. It'll be interesting to see how all the jumping between real and complex bundles, forms and cohomology will work out.

[Johan Commelin]

Well, to be fair, I don't think there's any roadmap written down anywhere.

[Johan Commelin]

Have you already played around with Lean a bit?

[Gunnar Þór Magnússon]

A little. I've done the natural numbers game and the intermediate value theorem tutorial. I just finished reading through the docs and am looking around in mathlib to see how some more complicated structures are done. I wanted to formalize something simple on my own, like maybe basic incidence geometries or groups, before trying to see if there was any low-hanging fruit in mathlib.

[Kevin Buzzard]

Maybe some of the workshops at https://github.com/ImperialCollegeLondon/formalising-mathematics are now helpful? Alternatively it's a very good idea to just choose a project of your own, ask for help with the definitions (because they make or break the project), and then try to prove the theorems yourself.

[Gunnar Þór Magnússon]

Those look pretty great, actually. Thanks!