Hi. I'm Gareth McCaughan. I've been a consistent reader and occasional commenter since the Overcoming Bias days. My LW username is "gjm" (not "Gjm" despite the wiki software's preference for that capitalization). Elsewehere I generally go by one of "g", "gjm", or "gjm11". The URL listed here is for my website and blog, neither of which has been substantially updated for several years. I live near Cambridge (UK) and work for Hewlett-Packard (who acquired the company that acquired what remained of the small company I used to work for, after they were acquired by someone else). My business cards say "mathematician" but in practice my work is a mixture of simulation, data analysis, algorithm design, software development, problem-solving, and whatever random engineering no one else is doing. I am married and have a daughter born in mid-2006. The best way to contact me is by email: firstname dot lastname at pobox dot com. I am happy to be emailed out of the blue by interesting people. If you are an LW regular you are probably an interesting person in the relevant sense even if you think you aren't.
If you're wondering why some of my very old posts and comments are at surprisingly negative scores, it's because for some time I was the favourite target of old-LW's resident neoreactionary troll, sockpuppeteer and mass-downvoter.
I'm pretty sure what's going on is:
It would be nice to have this more explicitly from the AlphaProof people, though.
[EDITED to add:] Actually, as per the tweet from W T Gowers quoted by "O O" elsewhere in this thread, we do have it explicitly, not from the AlphaProof people but from one of the mathematicians the AlphaProof people engaged to evaluate their solutions.
The AlphaZero algorithm doesn't obviously not involve an LLM. It has a "policy network" to propose moves, and I don't know what that looks like in the case of AlphaProof. If I had to guess blindly I would guess it's an LLM, but maybe they've got something else instead.
I don't think this [sc. that AlphaProof uses an LLM to generate candidate next steps] is true, actually.
Hmm, maybe you're right. I thought I'd seen something that said it did that, but perhaps I hallucinated it. (What they've written isn't specific enough to make it clear that it doesn't do that either, at least to me. They say "AlphaProof generates solution candidates", but nothing about how it generates them. I get the impression that it's something at least kinda LLM-like, but could be wrong.)
Nothing you have said seems to make any sort of conspiracy theory around this more plausible than the alternative, namely that it's just chance. There are 336 half-hours per week; when two notable things happen in a week, about half a percent of the time one of them happens within half an hour of the other. The sort of conspiracies you're talking about seem to me more unlikely than that.
(Why a week? Arbitrary choice of timeframe. The point isn't a detailed probability calculation, it's that minor coincidences happen all the time.)
Given how much harm such an incident could do CrowdStrike, and given how much harm it could do an individual at Crowdstrike who turned out to have caused it on purpose, your second explanation seems wildly improbable.
The third one seems pretty improbable too. I'm trying to imagine a concrete sequence of events that matches your description, and I really don't think I can. Especially as Trump's formal acceptance of the GOP nomination can hardly have been any sort of news to anyone.
(Maybe I've misunderstood your tone and your comment is simply a joke, in which case fair enough. But if you're making any sort of serious suggestion that the incident was anything to do with Mr Trump, I think you're even crazier than he is.)
Right: as I said upthread, the discussion is largely about whether terms like "spending" are misleading or helpful when we're talking about time rather than money. And, as you point out (or at least it seems clearly implied by what you say), whether a given term is helpful to a given person will depend on what other things are associated with that term in that person's mind, so it's not like there's even a definite answer to "is it helpful or misleading?".
(But, not that it matters all that much, I think you might possibly not have noticed that Ruby and Raemon are different people?)
In such a world we'd presumably already have vocabulary adapted to that situation :-). But yes, I would feel fine using the term "spending" (but then I also feel fine talking about "spending time") but wouldn't want to assume that all my intuitions from the present world still apply.
(E.g., in the actual world, for anyone who is neither very rich or very poor spending always has saving as an alternative[1], and how much you save can have a big impact on your future well-being. In the hypothetical spend-it-or-lose-it world, that isn't the case, and that feels like a pretty important difference.)
[1] For the very poor, much of their spending is basically compulsory and saving instead isn't an option. For the very rich, the choice is still there but for normal-size purchases matters less because they're going to have ample resources whether they spend or save.
I am not convinced by the analogy. If you have $30 in your bank account you spend it on a book, you are $30 poorer; you had the option of just not doing that, in which case you would still have the $30. If you have 60 minutes ahead of you in the day and you spend it with a friend, then indeed you're 60 minutes older = poorer at the end of that time; but you didn't have the option of not spending those 60 minutes; they were going to pass by one way or another whatever you did.
You might still have given up something valuable! If you'd have preferred to devote those 60 minutes to earning money, or sleeping, or discovering timeless mathematical truths, then talking to your friend instead has had an opportunity cost. But the valuable thing you've foregone is that other thing you'd prefer to have done, not the time itself. That was always going to pass you by; it always does.
There aren't exactly definite right and wrong answers here; everyone agrees that "spending" time is not exactly the same thing as spending money, ditto for "giving" time, and the question is merely whether it's similar enough that the choice of language isn't misleading us. And it seems to me that, because the time is going to go anyway, the least-misleading way to think of it is that the default, no-action, case to compare with -- analogous to simply not spending money and having it sit in the bank -- is whatever you'd have been doing with your time otherwise. If you help a friend out by doing some tedious task that makes their life better, then you are "giving" or "spending" time. If you sit and chat with a friend because you both enjoy talking with one another, then you're not "giving" or "spending" in a sense that much resembles "giving" or "spending" money: you aren't worse off afterwards than if you hadn't done that; if you hadn't, then you'd likely have occupied the same time doing something no better.
I'm in two minds as to whether I believe what I just wrote. The counter-argument goes like this: comparing the situation after spending an hour with your friend with the situation after spending an hour doing something else begs the question; it's like comparing the situation after spending the $30 on a book with that after spending the $30 on something else. But I don't think the counter-argument really works, precisely because you have the option of just leaving the $30 in the bank and never spending it on something else, and there is no corresponding option for money.
So maybe e.g. the (not very auto-) autoformalization part produced a theorem-statement template with some sort of placeholder where the relevant constant value goes, and AlphaProof knew it needed to find a suitable value to put in the gap.