Smaug123

Sorry, I assumed the inductive construction was implied; you can indeed describe properties of that particular interesting problem (though of course you can’t hold its definition in your head), so it goes in the list. Keep going. At some point you’ll hit problems where the process of constructing the problem doesn’t even fit in a brain, etc. There are at least countably many problems, but finitely many problems which any algorithm-which-fits-in-the-brain can describe given finitely many inputs-which-fit-in-the-brain.

This isn’t an enormously important point - the actual question at issue is an empirical one, “in a steady state, can we produce interesting problems at a rate that exceeds our ability to solve them and integrate our understanding” or something like that - but I did rankle at a “trivial” proof which is invalid due to equivocating between multiple definitions of the word “interesting” (which should really take an object, “interesting to me” vs “interesting to something smarter than me”).

An interesting problem must have a description that fits in a brain, at least for now. Your description-length argument assumes arbitrarily large storage.

I'd be interested in hearing a field report on this! For example, I can easily imagine that they're great at walking through the proof step by step, explaining background as necessary; but as TFA notes, one of the most important questions is "why is this definition the way it is?", and my bet would be that the Lean is not enough to help the LLMs meaningfully in answering that.

I mean, I was intending to supply the words that would link the LLM’s explanation to a more normal one, not to explain it; apparently that was extremely unclear. An actual explanation is much longer, as indeed I attempted to indicate by pointing to Wikipedia and saying that it might be more clear.

“Doing better than a totally useless explanation in fewer characters” is in general impossible, of course, eg if the first explanation has only one character.

(Apparently I was extremely unclear with this text. For clarity: if you want to actually understand surreal numbers, go and read On Numbers and Games, by Conway, which is a delightful book; or get an LLM to talk you through Wikipedia. Original text follows.)

It’s a terrible explanation. A surreal number is defined as a pair of sets of surreal numbers (where you fiddle around the recursion in that definition by defining them in waves, so strictly speaking you’re defining “the surreal numbers born at time T” for each individual T given access to the surreal numbers born at all earlier times, and then you “take the union across all times”, scare quotes because there are too many times for this to result in a set). Zero is a surreal number but the LLM is using the word “zero” to mean “the set containing just the surreal number 0”; “nothing” here is the LLM’s obtuse word for the empty set. Wikipedia may actually be easier to follow.

This is probably not necessarily true. “f: list[1 A] -> list[A] pure, worst-case time n log n, such that for all x and 0 <= i <= j < len(x), f(x)[i] <= f(x)[j]” is probably good enough for nearly everyone unless the program synthesiser is actively adversarial; probably 99.999% of the list-sorting in the world is done via standard library functions anyway, which suggests that people don’t much care exactly how it happens.

The question pertinent to your decision is "do I want to see more of this on Hacker News, or less?".

Would it? Don’t they all desperately want more compute, and not the banning of new data centres?

I don’t have skin in this game, being from the increasingly oppressive UK and not the USA, but:

> what do you want to defend

Accuracy, and in this case people correctly knowing that their rights stem from some source (if they do! I don’t know the legal facts) or knowing the appropriate venue in which to campaign for them, rather than incorrectly believing that they don’t have rights and/or can’t get them.

> why do you want to defend it

Because words still have meanings, and people pretending they don’t, while screaming in ever more shrill tones at each other, is extremely tiresome, and the Internet is full of it.

As the article says, the situation in Jackson was deplorable; and it is indeed mind-boggling (to my puny European mind) that the same constitution which grants freedom of speech and the press was also not intended to grant the right to receive only believed-correct information from the government. But the ruling, for example, is not quoted as making any mention of any federal laws? The headline may be true for all I know, but the article provides only evidence for its truth about one particular source of rights.

Sorry, I think your pull quote is actually contradicting your gloss. Again, the pull quote states that it doesn’t infringe any constitutional right, not that it doesn’t infringe any rights granted for any other reason?

Does it? I think that conclusion requires observing additionally that all federal law also fails to grant a right to safe drinking water, doesn’t it?

Misleadingly provocative headline, right? The actual ruling from the article is that the US Constitution does not by itself grant US citizens that right. As the article itself points out, there’s nothing stopping other agreements from granting the right, and indeed several states do so explicitly.

It’s an aggregated list, not a list of formalisations in Lean - the checkbox is “things formalised in any prover”.

Because you wrote:

> what are exactly rules, which could be separate topic of research, this detail is skipped

I am now confident you’re a troll, though, so I am going to bow out.