I mean, that's exactly what a "slur" is. They are not coined with the recipient's comfort in mind, and saying them can sometimes provoke exactly the sort of fight you imagine.

But yes, violent consequences ought to be particularly unsurprising to an American, since the US is, by Western standards, an exceptionally violent country. [1]

[1] https://pmc.ncbi.nlm.nih.gov/articles/PMC9535176/ (table 2)

If you have time, can you elaborate or give some examples of mathematical nuances?

I am evaluating Sol and Fable on a fairly large dataset of subtly flawed informal mathematical arguments (task is to identify and name propositions with substantially incorrect proofs in a larger body of text), and Sol is saturating the benchmark, while Fable is below 50% even with the most generous grading.

I don't work in the natural sciences, so I suspect you mean something different by "mathematical nuance".

But one can already study the consequences of P=NP right now. You don't need to know that it's provably true in order to do that.

Knowing an actual proof would be useful, but an oracle revealing merely that it's true (or even provable) without telling you the proof does not let you do anything you couldn't do before.

As in, you were using state of the art generator X, and you couldn't see the performance bottleneck, but updating to a newer (faster, or same speed but higher quality) generator Y, and could subsequently identify the performance bottleneck?

If you're using PCG, not in the last 12 years.

(In a parallel comment I suggest trying AES-CTR for this use case)

Have you skimmed the linked thread?

> especially simulation/sampling approaches that are bound by the number and quality of uniform variates per second

Sorry, nobody does stochastic simulations where the number of uniform random numbers obtained per second is any sort of bottleneck. If you've spent considerable time on stochastic simulation, you already know this.

But even if you insist that you alone are doing some very weird stochastic simulation which is somehow bottlenecked on sourcing random numbers fast enough, the falling in planes phenomenon linked above would make xorshift-type generators a poor choice for most sorts of simulations. It introduces spatial correlations into any sort of lattice dynamics simulation (Ising model, percolation) and every high dimensional Monte Carlo integration. Beyond falling in the planes, since xorshift is linear over GF(2), it is also a particularly bad choice for nondeterministic cellular automata and Boolean dynamical systems which use parity, bit masks, or xors.

AES-CTR throughput on a modern CPU is higher than that of xoshiro256++, and much higher quality. No advances in non-CS PRNGs can beat that while maintaining the same quality. If your stochastic simulation is bottlenecked on random bits, CSPRNGs are still the way to go, and they don't interact in nasty ways with any dynamical system you can actually sinulate quickly.

There is no real use case for better non-CS generators, as explained by adrian_b back in 2021 [3].

[1] https://en.wikipedia.org/wiki/RANDU [2] https://arxiv.org/abs/1908.10020 [3] https://news.ycombinator.com/item?id=28886698

No. Many engineers AND mathematicians worked for a long time to get us to a stage where Amazon can solve a billion SMT problems a day. To contribute, all of them had to understand the theory this article calls overrated.

The Aug 6 update has forced the entry box to auto-format Markdown in an attempt to imitate Claude. The implementation is buggy and even simple copy-and-paste has gone entirely haywire. They also forgot to leave a switch to turn the confounded autoformatting thing off.

Chat mode in general is currently crawling with more UX bugs than a porch screen in summer.

The same analysis applies: the probe tells us what the LLM thinks about the truth value if the sentence, not the truth value of the sentence. I don't think anyone claimed that these probes were truth oracles.

[1] https://smbc-comics.com/index.php?id=3657

The "generated kernel" refers to a "geometric modeling kernel", which has absolutely nothing to do with the proof-checking kernel that the de Bruijn criterion talks about. The proof can be verified by Lean's ordinary proof-checker, or external checkers.

Indeed. The last bug I fixed in a production app was one where people could not restore from backup due to a de/serialization issue. The correct behavior would have been straightforward to specify (round-tripping). Trying to verify the serializer against the correct behavior would have forced the devs to think through all the edge cases.

Why do you look at the speck of sawdust in your brother's eye and pay no attention to the plank in your own?

> I’m sure a prolog program can express whatever property you’re attempting to write just as tersely

No, you won't be able to express the most basic properties in Prolog at all, let alone as tersely as in a proper specification language.

E.g. if you have a language interpreter and a bytecode interpreter, pretty much every specification language will let you express the correctness of a compiler `compile(x)` as

``` for all scripts x and inputs i,

bytecodeInterpreter(compile(x),i) == languageInterpreter(x,i) ```

Good luck expressing this in Prolog, let alone equally tersely.

Well, mathematicians not working for Anthropic/OpenAI are heavily disincentivised from reporting that their discoveries were made using AI. If e.g. the idea that resolved the Mahler conjecture came from AI, it's not like we'd ever know.

I suspect the difficulty here lies more with your reading of the quoted sentence. British grammar school education, for all the years it devotes to the enterprise, does not always succeed in teaching reading comprehension.

You seem to be treating two rather different propositions as though they were one and the same. If text in general is not sufficiently information dense to support decoding some _arbitrary_ signal of provenance, that hardly establishes that no _specific_ passage can carry distinctive markers of provenance.

For example, you can recognize the unmistakable cadence of the California undergraduate. Impressive. Alas, even in your own example, when your British friends are "giving themselves away", you resort to an external signal, beyond the text, to determine provenance! That is, unless the text itself is claiming that its author is British (like the bots who claim they're John Horsetrader from Arkansas oblast).

When you have to decide whether a 2010s era SAT essay was from a SAT prep book author or an LLM prompted to write such an essay, you will struggle to distinguish one from the other. Not all texts have provenance signals. This is what it means for text to simply not be information dense enough to be able to decode some arbitrary signal of provenance from it.

I don't think the current nuclear doctrines are anywhere close to perfect or best possible. There is surely room for improvement. But I vehemently oppose more countries innovating on nuclear doctrine, because the average outcome of innovation is likely to be worse than the current equilibrium, for bystanders and innovators alike.

Medieval Europeans knew that the fallow-field system was imperfect, but many simultaneous experiments on alternatives would have led to famine, not viable alternatives. Careful experimentation in some monastery gardens is a good thing, but wagering everyone's supper on untested ideas isn't.

The same applies to our own civilization. Western capitalist culture has flaws aplenty. But this does not mean we should throw open the gates to every, or even any, alternative group that comes along.