This stream is not world-readable

Stream: FLT-regular

[Kevin Buzzard]

Tao's #Polynomial Freiman-Ruzsa conjecture stream was world-readable, and I certainly plan on making the FLT stream which I use for FLT-Wiles world-readable. But this stream isn't. If we make it public do all the old messages then become public? Shall we just change it back to FLT-regular and make a new world-readable FLT?

[Chris Birkbeck]

Oh I didn't know it wasn't public. But maybe it's best to revert and make a new one then.

[Alex J. Best]

Its public for people with a zulip account, just they have to sign in. I don't know the answer to Kevin's question, sounds like one for #Zulip meta , but I'm sure nobody here would mind as all messages here are essentially public anyways

[Chris Birkbeck]

I guess the problem is that if they are visible, then someone new looking at the stream might find it hard to see the split between the projects. Someone might come on a try and prove Hilbert 92 again! (Although I do expect in practice this isn't too much of a risk( the getting confused, not the Hilbert 92 thing))

[Kevin Buzzard]

/poll Should we rename this stream back to FLT-regular and make a new world-readable FLT stream?
Yes
No let's do something else (explain below)

[Kevin Buzzard]

I want to start doing things! I'm writing Lean code and have questions.

[Kevin Buzzard]

I have a cool question about implementing a lemma about Frey curves which is really trivial to explain but my Lean justification is horrible :-/

[Johan Commelin]

I suggest we wait for @Riccardo Brasca's opinion. I'm happy to create the new stream if he agrees.

[Riccardo Brasca]

Ok for me!

[Johan Commelin]

Ok, here's the new stream: #FLT