Smaug123

3 ms·

1.
by Smaug123 5d ago
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 po
2.
by Smaug123 6d ago
An interesting problem must have a description that fits in a brain, at least for now. Your description-length argument assumes arbitrarily large storage.
3.
by Smaug123 7d ago
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 q
4.
by Smaug123 8d ago
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 p
5.
by Smaug123 8d ago
(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. Origi
6.
by Smaug123 8d ago
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 s
7.
by Smaug123 15d ago
The question pertinent to your decision is "do I want to see more of this on Hacker News, or less?".
8.
by Smaug123 17d ago
Would it? Don’t they all desperately want more compute, and not the banning of new data centres?
9.
by Smaug123 20d ago
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
10.
by Smaug123 20d ago
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 rece
11.
by Smaug123 20d ago
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?
12.
by Smaug123 20d ago
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?
13.
by Smaug123 20d ago
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 gra
14.
by Smaug123 21d ago
It’s an aggregated list, not a list of formalisations in Lean - the checkbox is “things formalised in any prover”.
15.
by Smaug123 21d ago
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.
16.
by Smaug123 21d ago
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 countere
17.
by Smaug123 21d ago
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 t
18.
by Smaug123 21d ago
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
19.
by Smaug123 21d ago
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!
20.
by Smaug123 21d ago
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,
21.
by Smaug123 21d ago
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 the
22.
by Smaug123 21d ago
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
23.
by Smaug123 21d ago
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, slig
24.
by Smaug123 22d ago
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 L
25.
by Smaug123 22d ago
I claim that the percentages add up to more than 100% because the first described case overlaps with the second.
26.
by Smaug123 25d ago
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: Ant
27.
by Smaug123 25d ago
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 cla
28.
by Smaug123 28d ago
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 (&quo
29.
by Smaug123 29d ago
> 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 f
30.
by Smaug123 1mo ago
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,

More ›