Timeline for Should Kevin Buzzard's Lean question be left in its original state?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 23, 2018 at 1:28 | comment | added | Ben Burns | I upvoted this to support my concern that I don't want to see MO overrun with spammy project posts. However, I don't think Kevin Buzzard crossed "the line" (a fuzzy ambiguous thing), and thought his post was just barely acceptable for being a good fit for the community (and in fact contributes to the community for some of the reasons he outlines). Perhaps he gets the benefit for being first, but ... I think if there were a bunch of similar posts that start showing up I would voice concern on meta. But this question, in this particular instance, I think is ok. | |
| Sep 22, 2018 at 17:03 | comment | added | Dima Pasechnik | cf. meta.mathoverflow.net/a/3892/11100 | |
| Sep 22, 2018 at 16:44 | comment | added | Kevin Buzzard | I put it there in an attempt to show that the "obviously completely impossible task for a 1st year undergraduate" of learning how to formalise mathematics was now much easier than it used to be. I put it there to show that formalisation is now for the normal mathematician. I completely agree that it reads like an advert. I think it is desperately important for the mathematics community to understand it. I understand your point of view. As I already said, I just blogged all the information after you deleted it. I played no role in either the deletion or undeletion and don't know what is best. | |
| Sep 22, 2018 at 14:55 | comment | added | Federico Poloni | @KevinBuzzard I think that the question and this motivation are good, and should stay on MO. What I disagree is only the last section, which has no role in the question and is there just to raise the visibility of Lean. MO is a site to ask questions and give answers, not a blog or a news site where you post to get your project known. | |
| Sep 22, 2018 at 14:26 | comment | added | Kevin Buzzard | The original motivation behind the question is that I wanted to get a feeling from a broader community of mathematicians as to the kind of values of X which would make them think "hey! Lean now has X in it!". Already there is discussion on the Lean chat about formalising the statement of the classification of finite simple groups and which goals are actually going to be achievable. That was one of the main aims of the post. Of course another aim is trying to raise the visibility of Lean and maybe of theorem provers in general, and this is because I believe mathematicians need to know! (2/2) | |
| Sep 22, 2018 at 14:22 | comment | added | Kevin Buzzard | Here is some background. We are a loose-knit community of mathematicians and computer scientists with a vast amount of synergy. I have strongly argued on the Lean chat that the computer scientists should be devoting a lot more time formalising the mathematics that mathematicians are actually interested in and a lot less time formalising the mathematics which fits best into their theorem provers for whatever reason. What has happened in practice is that we are now formalising the kind of mathematics which the mathematicians among us are interested in e.g. perfectoid spaces. (1/2) | |
| Sep 22, 2018 at 14:18 | comment | added | Kevin Buzzard | xenaproject.wordpress.com/2018/09/22/… -- when you deleted the question I guessed that your thoughts would be what you have written above, and I wrote a blog post. | |
| Sep 22, 2018 at 13:50 | history | edited | Federico Poloni | CC BY-SA 4.0 |
deleted 3 characters in body
|
| Sep 22, 2018 at 13:35 | history | edited | Federico Poloni | CC BY-SA 4.0 |
added 167 characters in body
|
| Sep 22, 2018 at 13:25 | history | answered | Federico Poloni | CC BY-SA 4.0 |