website

Stream: Lean for the curious mathematician 2020

[Johan Commelin]

I would be happy to move the website to a place where other people can also edit.

[Jalex Stark]

where is the website?
here : https://math.commelin.net/2020/lftcm/

[Johan Commelin]

I would like to get this back into action. Where should the new website live? Some github.io site?

[Patrick Massot]

I think you can have a repo in the lean community organization and the website will automatically look like a subsite of the community site

[Johan Commelin]

Sounds good to me

[Johan Commelin]

https://github.com/leanprover-community/lftcm2020
@Patrick Massot you are already admin
@Jalex Stark I've invited you for write access

[Johan Commelin]

Should we steal/reuse/copy the Lean Together stylesheet, so that the website looks like a Lean file?

[Patrick Massot]

Reusing jokes is usually a bad idea.

[Patrick Massot]

I also don't think it carries a very welcoming message for real beginners that would only understand they don't have the prerequisite

[Johan Commelin]

Fair enough

[Jalex Stark]

I copied some material from your old website onto the readme in the git project.

I think the next step in organizing this thing is to form a strong-enough idea of what content will happen that week, and then to get commitments from people to do that thing.

[Johan Commelin]

Oooh thanks! Today might be a really good day for me to work on this.

[Johan Commelin]

Please add your name to the list of organisers if you feel like it. You've certainly already helped a lot with brainstorming (and motivating me).

[Johan Commelin]

Also... I guess "Local" in "Local organiser" doesn't really make sense anymore :wink:

[Johan Commelin]

Jalex Stark said:

I think the next step in organizing this thing is to form a strong-enough idea of what content will happen that week, and then to get commitments from people to do that thing.

I agree with this. I'll try to think about it (-;

[Patrick Massot]

I just received advertisement for an online meeting mixing pre-recorded talks with live talks at https://sites.duke.edu/scshgap/moduli-of-special-holonomy-metrics-and-their-periods/ Maybe there are organization ideas to steal there (I haven't looked at the organization details).

[Johan Commelin]

Thanks @Patrick Massot We'll take a look at it

[Alex J. Best]

Johan Commelin said:

Jalex Stark said:

I think the next step in organizing this thing is to form a strong-enough idea of what content will happen that week, and then to get commitments from people to do that thing.

I agree with this. I'll try to think about it (-;

One thing I think would be really cool is a session some sort of pair/trio/quadruplet programming, where a few "curious mathematicians" and a "proficient lean user" get in a zoom/BBB call for an hour say with the aim of each of the curious mathematicians formalizing one definition or theorem statement from their field. The idea is to have a more personal and condensed version of the interactions we often have on the zulip where questions can have a more fluid question/answer cycle with screensharing and extended conversation. the ratio of lean users to mathematicians of course will have to depend on the signups!

[Patrick Massot]

This will work only if the proficient Lean users know the topics in advance

[Alex J. Best]

Do you mean that they should already understand the topic? Or just have some prior warning enough to look up the wikipedia page? Of course it depends on the topic, if the definition is hypergraphs or matroids or some separation axiom for topological spaces its going to be way more possible than manifolds with boundary, but I'm hoping everyone has something in their field they might present the definition of in a colloquium talk for instance. But I'm really thinking of an interactive conversation where the lean user doesnt necessarily know the answer immediately!

[Alex J. Best]

And of course if the interested mathematician is an undergraduate or school student (ie no giving colloquium talks!) then hopefully whatever definition they're interested in is also on wikipedia or fairly well known.

[Kevin Buzzard]

When someone asks me how to do something I don't understand, I usually just dig down and down until I find something I do understand

[Johan Commelin]

@Alex J. Best Yes, that's a really good idea.

[Johan Commelin]

@Alex J. Best https://github.com/leanprover-community/lftcm2020/issues/5

[Johan Commelin]

Thanks to @Patrick Massot we now have the basics of a website: https://leanprover-community.github.io/lftcm2020/

[Yury G. Kudryashov]

https://github.com/leanprover-community/lftcm2020/pull/6

[Yury G. Kudryashov]

There was a simple quest: find out which repo should be the target of the PR.

[Floris van Doorn]

@Johan Commelin when googling, https://math.commelin.net/2020/lftcm/ is the first result I find, and it should link/redirect to https://leanprover-community.github.io/lftcm2020/

[Johan Commelin]

Aah good point! I'll do that

[Johan Commelin]

I think I managed to instruct my nginx to 301 redirect to the new site.

[Floris van Doorn]

It works!

[Heather Macbeth]

Could you also correct your differential geometry speaker? And Yury's surname is spelled differently than I have usually seen it (which does not necessarily mean that it is spelled wrong).

[Patrick Massot]

Fixed, thanks.

[Yury G. Kudryashov]

@Heather Macbeth Russian authorities have at least 3 different opinions on the correct spelling of my name/surname as can be seen from my 3 passports (yes, the idea "reuse the transliteration we used last time" is too hard for them).