robinhouston

What's the story behind the Great Unfuckening that took place between v4.18-rc8 and v5.6?

This definitely needs some context for the non-logicians in the house! Gödel's second incompleteness theorem shows that, if PA can prove its own consistency, then PA is inconsistent (and can therefore prove anything, including false things).

The work linked here doesn't show that PA is inconsistent, however: what it does is to define a new, weaker notion of what it means for PA to “prove its own consistency” and to show that PA can do that weaker thing.

Interesting work for sure, but it won't mean anything to you unless you already know a lot of logic.

If you want a language for expressing constraint satisfaction problems that's higher-level than SAT, I think MiniZinc is pretty interesting. https://www.minizinc.org/

Wow, that's a cool trick. So it _can_ be done using only builtins! Thanks for sharing.

> I hate it when people quote text as images because it makes it impossible to cut and paste.

That's much less true than it used to be! I don't know what device you're using, but on my iPhone I can seamlessly copy the text from that image.

That's ok, but %1 will refer to the wrong job if there's already a background job running. You could use %% instead, but that will refer to the wrong job if <command> terminates before the timeout.

I’ve been playing around with trying to make a timeout using just bash builtins, motivated by the fact that my Mac doesn’t have the timeout command.

I haven’t quite been able to do it using _only_ builtins, but if you allow the sleep command (which has been standardised since the first version of POSIX, so it should be available pretty much anywhere that makes any sort of attempt to be POSIX compliant), then this seems ok:

  # TIMEOUT SYSTEM
  #
  # Defines a timeout function:
  #
  # Usage: timeout <num_seconds> <command>
  #
  # which runs <command> after <num_seconds> have elapsed, if the script
  # has not exited by then.

  _alarm() {
      local timeout=$1

      # Spawn a subshell that sleeps for $timeout seconds
      # and then sends us SIGALRM
      (
          sleep "$timeout"
          kill -ALRM $$
      ) &

      # If this shell exits before the timeout has fired,
      # clean up by killing the subshell
      subshell_pid=$!
      trap _cleanup EXIT
  }

  _cleanup() {
      if [ -n "$subshell_pid" ]
      then
          kill "$subshell_pid"
      fi
  }

  timeout() {
      local timeout=$1
      local command=$2

      trap "$command" ALRM
      _alarm "$timeout"
  }

  # MAIN PROGRAM

  times_up() {
      echo 'TIME OUT!'
      subshell_pid=
      exit 1
  }

  timeout 10 times_up

  for i in {1..20}
  do
      sleep 1
      echo $i
  done

Congratulations, Lone Coder! Both for the exciting work and for getting it on the front page of the FT. Just amazing on both counts.

Thanks. What's particularly embarrassing is that I found that submission this morning, and read the comments on it, and then somehow forgot about its existence until you reminded me of it just now.

It was a fun surprise to see this story on the front page of this morning's Financial Times. It's very unusual in my experience for this sort of thing to be picked up by the mainstream media before it's on HN or similar. I wonder how the FT reporter came across the story.

I had fun with that! I'm happy someone appreciates it.

S3's support of the Range: header makes it possible to do that sort of thing remarkably cheaply and efficiently.

Using other constants in place of the ‘4’ can lead to some _really_ gigantic smallest solutions: https://observablehq.com/@robinhouston/a-remarkable-diophant...

From some conversations on Twitter, it seems plausible that the rank-48 decomposition of the 4×4 matrix multiplication tensor really is new; and that perhaps where things have gone awry is attempting to summarise this result in a more lay-friendly manner: the algorithm in that post apparently doesn't constitute or imply a rank-48 tensor decomposition.

On the other side, it's claimed here that an algorithm that uses only 46 multiplications has been known since 1970: https://mathstodon.xyz/@fredrikj/114508287537669113

The proof that it stops instead of going on forever is here: https://arxiv.org/abs/0908.3724

It’s more than 200 pages of pretty technical mathematics, so I’m reasonably confident that there is no description a layperson might understand.

> One woman (I don't know her name)

Amanda Askell https://askell.io/

The interview is here: https://www.youtube.com/watch?v=ugvHCXCOmm4&t=9773s

I would encourage anyone who's intrigued by this paradox to read Timothy Chow's comprehensive paper on the subject (https://arxiv.org/abs/math/9903160).

In particular, he discusses what he calls the meta-paradox:

> The meta-paradox consists of two seemingly incompatible facts. The first is that the surprise exam paradox seems easy to resolve. Those seeing it for the first time typically have the instinctive reaction that the flaw in the students’ reasoning is obvious. Furthermore, most readers who have tried to think it through have had little difficulty resolving it to their own satisfaction.

> The second (astonishing) fact is that to date nearly a hundred papers on the paradox have been published, and still no consensus on its correct resolution has been reached. The paradox has even been called a “significant problem” for philosophy [30, chapter 7, section VII]. How can this be? Can such a ridiculous argument really be a major unsolved mystery? If not, why does paper after paper begin by brusquely dismissing all previous work and claiming that it alone presents the long-awaited simple solution that lays the paradox to rest once and for all?

> Some other paradoxes suffer from a similar meta-paradox, but the problem is especially acute in the case of the surprise examination paradox. For most other trivial-sounding paradoxes there is broad consensus on the proper resolution, whereas for the surprise exam paradox there is not even agreement on its proper formulation. Since one’s view of the meta-paradox influences the way one views the paradox itself, I must try to clear up the former before discussing the latter.

> In my view, most of the confusion has been caused by authors who have plunged into the process of “resolving” the paradox without first having a clear idea of what it means to “resolve” a paradox. The goal is poorly understood, so controversy over whether the goal has been attained is inevitable. Let me now suggest a way of thinking about the process of “resolving a paradox” that I believe dispels the meta-paradox.

Another very interesting article on the primality of 1 is Evelyn Lamb's _Why isn't 1 a prime number?_ (https://www.scientificamerican.com/blog/roots-of-unity/why-i...)

A slightly facetious answer might be that this is the wrong question to ask, and the right question is: when did 1 stop being a prime number? To which the answer is: some time between 1933 (when the 6th edition of Hardy's _A course in pure mathematics_ was published) and 1938 (when the 7th edition was published).

On the theme of difficult ideas explained using a limited vocabulary, I suppose one has to mention xkcd's Thing Explainer as well as George Boolos's classic _Gödel's Second Incompleteness Theorem Explained in Words of One Syllable_:

https://en.wikipedia.org/wiki/Thing_Explainer

https://languagelog.ldc.upenn.edu/myl/BoolosOneSyllable.pdf

I'm not trying to make either a moral or a legal argument, only to warn against using the term in a way that is liable to cause confusion or needless antagonism.

This is a complaint as old as the internet, which probably bears repeating from time to time.

One part I think is unnecessarily controversial:

> It does not mean it is free and open-source (FOSS).

This is another old argument that it's pointless to re-litigate, but one should at least note that this way of using the term ‘Open Source’ contradicts the OSI definition and risks causing avoidable misunderstandings.

https://opensource.org/osd

I would find this argument more compelling if it were supported by examples. Although it’s easy to imagine this sort of dynamic unfolding, offhand I can’t think of any good examples of it happening with internet protocols in quite this way.

On the other hand, I can immediately think of an example to the contrary: I would at least partly attribute the failure of XHTML to the fact that conforming renderers were forbidden to be liberal in what they accept, and viewers of XHTML pages would often be faced with an error message in place of the page they wanted to see, as a consequence of some minor mistake.

Of course we only have anecdotes here, but I think this is probably a real vibe shift that's happening in big tech. For all the talk of ‘masculine energy’, my feeling is that it actually reflects a loss of confidence: it reminds me very strongly of a similar cultural shift that I remember happening during the bursting of the dotcom bubble.

I don't see any contradiction between your claim that TPU v3 uses systolic arrays and the parent post's claim that TPU v4 does not.

I think the idea of all these is to make the file not be recognised as text (which doesn't allow nulls), ASCII (which doesn't use the high bit), UTF-8 (which doesn't allow invalid UTF-8 sequences).

Basically so that no valid file in this binary format will be incorrectly misidentified as a text file.

Bliss was it in that dawn to be alive, But to be young was very heaven!

— Wordsworth, _The French Revolution as It Appeared to Enthusiasts at Its Commencement_

I love your description of this heady time, which matches the way that I remember it. Surely there are at least pockets of such technological optimism in today's world – but fewer, I fear, and less confident.

To me the most sobering cautionary tale from the dotcom bubble is the story of Cisco. Cisco manufactured, in a very real sense, the physical infrastructure of the internet: the routers, switches, modems, etc. that directed the IP packets to their destinations. (To a significant extent they still do, though nowadays they have more competition in that area.)

Savvy investors piled in to the stock, reasoning that, while internet startups might come and go, the internet itself was surely here to stay. It was popular to observe that, in the California gold rush of the mid-1800s, the purveyors of mining equipment made it rich more reliably than the prospectors for gold.

Anyway the Cisco stock price peaked in March 2000, and to this day it still has not reached that level again. The savvy investors were of course correct in their belief that the internet would continue to be important, and that Cisco would continue to be an important manufacturer of internet networking equipment. But they lost money anyway, because once the euphoria had worn off the market consensus was that the stock just wasn’t worth as much as the price it had been selling for at the height of the mania.

Any parallels to hot contemporary stocks are left as an exercise for the reader — and I do not mean to suggest that history must always repeat exactly.

That’s not my experience of Australians at all! The Australians I’ve met (through working for an Australian company) all seem to love their nanny state, and genuinely don’t understand how anyone could see anything undesirable in it.

I know. My description was aimed at people who had never heard of Wikia, and certainly didn't understand its substructure. But I realise it sounds wrong to people like you who do understand that, and I wish I'd worded it more carefully.

I fear I'm responsible for this misconception. At first we didn't realise the proof had originated on 4chan – Nathaniel Johnston originally found the proof on Wikia, and the 4chan archive was only discovered later.

When I tweeted about it, I said “The best known lower bound for the minimal length of superpermutations was proved by an anonymous user of a wiki mainly devoted to anime.”, by which I meant Wikia (which was pretty anime-centric at the time).

I think, combined with the fact that the problem was posed to 4chan in terms of Haruhi, and because it makes a funnier story, that the anime angle has been a bit exaggerated.

Having said that, the author of the proof is not (to the best of my knowledge) a mathematician, nor does he have any apparent desire to publish his result in a conventional form, so it's still a pretty unexpected place for such a result to originate.