""But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway)."" lol if you say so buddy...
Hey! If you know more than others (which I'm guessing you do), that's great - but in that case can you please share some of what you know, so the rest of us can learn? If you only post a putdown, it just makes the thread mean and the rest of us don't get to learn anything.
Sure. We have this for countries, like "example.co.uk", so I made "name" be a country and it...just works (maybe).
You only get a first name and a last name and a .name though. You can't be robert.louis.stevenson.name - just louis.stevenson.name.
(Incidentally, this was a Claude suggestion. The change only took a couple minutes but figuring out what mechanism in the code could do this would have taken me a lot longer.)
While we have you here - I've seen this discussion multiple times - does @dang "do" anything to get your attention, or did you just happen to see it because you were scanning the comments manually, and therefore email is better for letting you know something?
Can you please transmute your frustration into thoughtful, interesting comments, rather than venting it into putdowns of others?
Since you're posting here, you're as much "the hackernews community" as the rest of us.
The intention of the site is clear: curious, substantive conversation (https://news.ycombinator.com/newsguidelines.html). We know better than anyone how easy it is to get derailed from this, but really the best thing to do is to practice thoughtful conversation even when others are not.
reply