Zulip Chat Archive

Stream: Lean for the curious mathematician 2020

Topic: website


Johan Commelin (May 13 2020 at 18:01):

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

Jalex Stark (May 15 2020 at 23:45):

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

Johan Commelin (May 28 2020 at 09:07):

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

Patrick Massot (May 28 2020 at 09:42):

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 (May 28 2020 at 09:42):

Sounds good to me

Johan Commelin (May 28 2020 at 09:45):

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

Johan Commelin (May 28 2020 at 09:45):

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

Patrick Massot (May 28 2020 at 09:48):

Reusing jokes is usually a bad idea.

Patrick Massot (May 28 2020 at 09:48):

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 (May 28 2020 at 09:48):

Fair enough

Jalex Stark (Jun 01 2020 at 08:08):

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 (Jun 01 2020 at 08:11):

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

Johan Commelin (Jun 01 2020 at 08:13):

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 (Jun 01 2020 at 08:13):

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

Johan Commelin (Jun 01 2020 at 08:14):

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 (Jun 01 2020 at 11:30):

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 (Jun 01 2020 at 11:56):

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

Alex J. Best (Jun 01 2020 at 14:34):

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 (Jun 01 2020 at 14:59):

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

Alex J. Best (Jun 01 2020 at 15:08):

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 (Jun 01 2020 at 15:11):

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 (Jun 01 2020 at 15:28):

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 (Jun 01 2020 at 16:27):

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

Johan Commelin (Jun 01 2020 at 16:29):

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

Johan Commelin (Jun 22 2020 at 13:55):

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

Yury G. Kudryashov (Jun 22 2020 at 20:33):

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

Yury G. Kudryashov (Jun 22 2020 at 20:34):

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

Floris van Doorn (Jun 26 2020 at 02:10):

@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 (Jun 26 2020 at 03:01):

Aah good point! I'll do that

Johan Commelin (Jun 26 2020 at 03:14):

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

Floris van Doorn (Jun 26 2020 at 03:15):

It works!

Heather Macbeth (Jun 26 2020 at 13:06):

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 (Jun 26 2020 at 13:30):

Fixed, thanks.

Yury G. Kudryashov (Jun 26 2020 at 14:26):

@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).


Last updated: Dec 20 2023 at 11:08 UTC