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.

As I have said a few times now, you should read any first course in set theory. I’m quoting my third-year notes from Cambridge there, but essentially every intro to set theory will say the same. (I’m sure someone will find a single counterexample that does it somehow differently.)

You don’t necessarily want concision for that. You want “the right abstractions”, with an API that admits nice general work building on top of it. That might mean doing things in more generality than you wanted to. For example, for a long time (and possibly even now, I’m not up to date) there was very little graph theory in mathlib because there wasn’t consensus about what “the right definition” of a graph was, to permit all the possible consumers to get what they need from the API.

The LLM is not the thing applying the logical rules. That is instead the deterministic system Lean 4. (Also that Apple paper was garbage even when it was written, assuming you’re referring to The Illusion of Thinking, and LLMs have got much better since.)

Fortunately FLT is an extremely simple statement. Much easier to satisfy yourself that its statement is what you wanted to say than it would be for most statements of interest!

Claude’s formalisation, being in Lean, is based on the calculus of inductive constructions, not ZFC. In Lean 3, per Carneiro, any theorem of Lean 3’s theory can be proved in ZFC plus some finite number of inaccessible cardinals (and, IIRC, vice versa). The precise strength of Lean 4 is not quite clear yet, I think (I guess this is partly what Lean4Lean is hoping to address).

It simply does have functions. According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element.

I mean this quite seriously: have you considered reading any first course in set theory?

Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.

I think this isn’t true? Comparator verifies proofs; it’s not clear to me what it even means to mechanically verify a statement to be valid. The statement is manifestly valid anyway - it’s hard to find much simpler statements of maths, slightly odd facts of mathlib’s natural arithmetic like the saturating behaviour of natural subtraction notwithstanding.

It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.

I claim that the percentages add up to more than 100% because the first described case overlaps with the second.

It doesn't necessarily change the output distribution; it depends exactly how it's implemented, and Anthropic haven't told us that. Google's original SynthID paper describes how you can do this.

Toy proof-of-concept: Anthropic owns a secret key which is a coin-flip Bernoulli random variable K with p=1/2. You are paying Anthropic to give you X, a Bernoulli random variable with p=1/2. Anthropic changes from their old strategy, "draw from K, then throw it away and flip a coin, each time you ask for a sample", to their new strategy, "draw from K and send it to you". You cannot observe the difference, but Anthropic knows K and so they know when you are repeating its outputs. (Obviously this is a toy example; in reality the distribution is vastly more complicated than Bernoulli, and Anthropic isn't just storing some model outputs to use as K but instead is computing a correlation with a known pseudorandomness source.)

G-Research | https://www.gresearch.com | London UK, on-site | Full-time

G-Research is a leading quant finance company. Big compute farm, interesting problems.

My team is hiring senior engineers to work on our (actually world class) DAG scheduling infra for distributing research and production workloads across the compute farm. What we do is roughly:

* maintain and improve the SDKs for that scheduler in Python, F#, and C#

* add interesting new features to the scheduler itself

* maintain and improve a web backend and UI for quants and engineers to monitor their jobs, increasingly with high availability requirements

* translate bidirectionally at the business level between low-level infra providers and quant/ML researchers

Some functional experience preferred, because our core product is in F#. Lots of dealing with very smart researchers and engineers, with the kind of fun problems arising when you run large ML workloads at scale.

[email protected] or my personal [email protected]

You didn't name the object when you said "let this thing be X"; you actually had already identified that "thing", and that process of identification was the process of naming it. You then defined some syntax ("X") and said that it was a name.

But there are things for which you can't even say "let 'this thing' be…". For example, ZF proves that there are uncountably many reals. There are only countably many names, so there must be unnameable reals. You can talk about "generic" reals (you can say "let x be a real" and do all sorts of interesting things with a generic x), but there are specific reals you will never be able to name specifically enough to distinguish them from their uncountably-many brethren. That doesn't make them "vague, undefined or ephemeral"! They're just so numerous that you can't describe the distinctions between them.

(Even hardcore constructivists usually accept enough Choice to prove the reals uncountable, although https://arxiv.org/abs/2404.01256 made headlines when it was shown not to be necessarily true.)

> no one has found one

More than that: there is no way to build one (assuming the word "build" means some concrete construction), because it's consistent with ZF that the reals admit no well-ordering. Indeed, you can use forcing to construct a model of R in which there is an infinite but Dedekind-finite subset of R; and you can't well-order such a set, because a well-ordering would turn it into an ordinal, and any Dedekind-finite ordinal is finite. You must use some sort of choice principle to construct a well-ordering. (Of course, it's consistent that they can be well-ordered, too, as you say; or e.g. under the hypothesis V=L, where there's even a canonical well-ordering given by the lexicographic well-ordering L comes with.)

I’m afraid human red-teamers against supposedly highly secure targets, with lots of protocols in highly policed settings, do frequently manage this kind of social engineering. There’s loads of stories of pentesting military establishments, for example.