To be totally honest, Lean isn't looking all that approachable, golfable nor particularly unique as opposed to other theorem provers, that is, not at the level we'll probably be able to get into in a month.
Wondering what you guys think of making all theorem proving langs within the scope of this LOTM?
We haven't had any as LOTM before, and I've hardly seen any on CGCC before.
More seriously though. People have upvoted it, that's an indication that people want it as LOTM. You might have a personal dislike of it, but it's the top post.
This would open the door to learning more mainstream langs like Agda & Coq, which seem interesting. But likewise, I don't think any of us will want to dedicate a whole month to golfing Agda. And then to golfing Coq. My sense is at the level that we use them on CGCC, some of the theorem provers might be a bit too similar.
(I don't know about Agda vs Coq specifically, but my sense is that there are at least a few big name ones out there that look very similar to Lean, while being more approachable and better documented.)
@cairdcoinheringaahing A friend of mine who worked at Starbucks wrote an Ed Sheeran parody a few years ago, so now my head is stuck in a repeating loop of "I'm in love with the pumpkin spice / I'm in love with the latte"
@AaronMiller do you know how much TP you get from Kris defending? Because you might want to find out that stat (by experimentation of course, don't look it up)
since it's past 4 in the morning and I just spent around 5 1/2 hours straight playing a game that is essentially sh*tposting with plot, i should prbly sleep now
In accordance with our meta agreement, since one candidate received more votes than the others, we have a new featured language! Throughout October 2021, our Language of the Month will be:
Lean
What's a Language of the Month?
See the meta post for nominations. In short, during October, those wh...
> In the past, questions could be made community wiki by their authors or by certain automatic triggers but now the only means is by a moderator converting it to community wiki
@pxeger I expected the entire internet to flood into this chat room and congratulate us on reaching this incredible and unique milestone, before giving us each $1m :P
Y'know, a reasonable and perfectly normal thing to expect :P
actually i was confused in the morning that why some where changing pfp and names then i open minecraft and see some things have changed and then i realise that it is the month of holloween
Chat Mega Challenge: There are currently 28530 starred messages. I will award a +100 bounty to the user who posts the 30000'th starred message, so long as it has 3+ stars
I like the fact that its clear that whoever went on a starring spree to get it to 3 clearly had no idea which message was the 30kth one and starred all the 2 star ones to be safe :P
In accordance with our meta agreement, since one candidate received more votes than the others, we have a new featured language! Throughout October 2021, our Language of the Month will be:
Lean
What's a Language of the Month?
See the meta post for nominations. In short, during October, those wh...
