saithound

> Why have we not seen an improvements in products? [..] Is everyone just running full speed in circles or something?

The simplest explanation is that they don't give a flying flamingo about what you or I consider "improvements to products".

This report is an example.

There are several changes that modify CI behaviour, where the article gives no corresponding quality measurement.

They replaced type aware custom lint rules with AST-only static analysis. They don't say anything about what those new rules detect, didn't do old-vs-new rule comparison. They switched the TypeScript check from tsc to tsgo. Again, they are very proud of the performance improvement, but don't seem to care about diagnostic equivalence. The list goes on. They don't even report pass/fail agreement between the old and the new CI. They have 4x more tests, but no idea whether this big test suite works any better than the smaller old one, or even whether it works at all.

You opened with the claim that nonstandard analysis hasn't caught on because it's "mostly the exact same arguments wrapped in slightly different language". I pointed out that the arguments are in fact very distinct: e.g. Nelson's proof of the intermediate value theorem is something that any NSA student would see, but no standard textbook teaches IVT by a standard language counterpart of it.

One post later, you answered that Nelson's IVT argument is in fact the "standard nested interval proof" with the limiting step rewritten in nonstandard language.

That claim is simply wrong. Why? Because Nelson's construction straightforwardly generalises to Brouwer, while the nested intervals proofs cannot. The discussion of reverse mathematics / computability is not a tangent, it explains precisely why Nelson's proof can generalise to give the BFPT in two dimensions, whereas the nested intervals proofs (which you claim is the same) cannot.

You then brought up that the BFPT generalisation of Nelson's argument needs the Sperner lemma as "crucial additional ingredient". Now you make the same point again:

> What I'm saying is that for the coloring proof of BFPT to work, whether clothed in standard or nonstandard language, you must perform a combinatorial argument that uses a topology of a triangle as a necessary ingredient, similar in shape to the proof of Sperner's lemma.

Presumably you keep pointing this out because you think it justifies some claim like '1D Nelson is actually nested intervals with the limiting step recast in nonstandard language, even if the 2D generalization of Nelson is not'.

But it does not. The combinatorial content is the same, the 1-dimensional interval case uses the topology of the domain just as much as the 2-dimensional triangle case does. The 2D argument wouldn't work on the annulus, and the 1D version would not work on the union of two disjoint intervals. The Sperner lemma is present in 1D, and present in 2D. If instead your point is only that proving the BFPT requires a harder case of the Sperner lemma than IVT, then of course it does. But what relevance does that have to the original claim that Nelson's IVT proof is the nested-interval proof? The proof of the Sperner lemma is pure combinatorics, it does not involve any (standard or nonstandard) analysis.

Or have you changed your mind on your earlier claim that Nelson's proof is "is the standard nested interval proof"?

If so, I think that's great, and closes the thread on whether NSA is largely the same arguments, since even the first proofs of the basic results are different.

If you still think that it's the nested interval proof, well, I am not sure what else to say, apart from linking the literature which studies this exact question, that I've already done, and that you dismissed as a tangent.

Either way, this discussion went on for too long at this point, so I won't monitor it further.

Not so relevant to this discussion, since if you are funded by patronage networks, you need to justify your work to your patron. If you are funded by grants or public research funds, you need to justify your work to the general public.

You made a sweeping claim that nonstandard analysis arguments are the exact same arguments, wrapped in nonstandard langauge. I explained that (while your other claims about simplicity may be valid) this is not so and detracts from the rest of your points. I challenged you to defend your "same arguments" claim by finding any standard analysis textbook which teaches a standard language version of Nelson's argument as a proof of the IVT. Let me recap what happened since then:

1. Two comments ago you confidently claimed that Nelson's IVT proof is "the standard nested interval proof" with the limiting step written in nonstandard language. That is a straightforward claim about the structure of the proof, one that you didn't bother to substantiate, and that is straightforwardly false.

2. After I explained why it's false (Nelson's construction proves BFPT, which no nested interval type proof can do), you changed your response: now the Sperner lemma was a "crucial additional ingredient". But Nelson's combinatorial step, that opposite endpoint colors force a blue-red interval, _is_ the one-dimensional instance of the Sperner lemma (and indeed the base case when you prove Sperner's lemma for arbitrary dimensional simplices by induction; the analytic part is independent of dimension, once you find an infinitesimal multicolored simplex, you take its common standard part and apply continuity exactly as before).

3. Then you wrote this:

> In the standard formulation, you apply the Sperner's lemma to find smaller and smaller triangles, and apply compactness, precisely as in the standard proof of intermediate value theorem.

There is a standard proof of Brouwer via the Sperner lemma, and it is _also_ not of the same form as the standard nested interval proof of the IVT. In the nested interval proof, you find a sign-change interval, then find a smaller sign-change interval inside it, and so on. The intersection of all of these contains a point, and that's your zero. Nelson's proof does not do this, and neither does the standard proof of Brouwer via the Sperner lemma: you do not, and cannot, take a 3-color interior triangle, then find a smaller 3-color interior triangle inside it and so on. Even the first step would not work, since the inherited labelling does not satisfy the right boundary condition relative to the small triangle!

And this is also why the computability paper I cited ("where I quote reverse mathematics stuff" ;) was very much relevant. There can be no effective "nested triangle" proofs of the Brouwer fixed point theorem at all, because such a proof would let you compute a Brouwer fixed point, and there are examples of computable maps on the triangle without computable fixed points. If Nelson's IVT proof was the nested interval proof, then swapping in the higher-dimensional Sperner step would give a nested-type proof of BFPT. No such proof can exist. Since Nelson's argument proves the BFPT without any change to the analytic part, it is not a nested interval type argument.

You first misidentified Nelson's proof as nested intervals, and then treated Sperner as an additional ingredient even though the coloring step in Nelson's proof is already the corresponding Sperner argument. Those are both fairly serious misunderstandings about these proof. Given this, I don't think our exchange leaves readers with much confidence in your assessment of NSA's drawbacks and benefits. That's a disappointing outcome, as far as I'm concerned. There are good arguments to make that NSA adds little value to undergraduate education, such as simplicity or the difficulty of the prerequisites, and good conversations to be had about them. But "NSA proofs are the same proofs wrapped in a different language" is not one, and I wish you had just narrowed it instead of doubling down.

> imagine yourself living in the 1700s. how would you justify Newton and Leibniz's work on calculus?

They didn't have to, as there were no state grants or public research funds for mathematics during the 17th century.

Newton supported himself from his inheritance throughout the Great Plague, while he invented calculus, and then from flat salaries as teacher, then flat salaries from working at the London Mint. He later became fabulously wealthy after his appointment as Master of the Mint.

Leibniz was a diplomat, then a librarian.

> This is the standard nested interval proof

It is not.

I'll be honest: your one sentence response tells me you did not read the proof above in any detail.

I chose Nelson's proof precisely because its construction is well-studied and well-understood. The same construction of a mesh containing all standard points, with the coloring forcing a tiny multicolored cell, extends from the interval to the triangle. In one dimension you get two adjacent differently colored points; in two dimensions you get an infinitesimal triangle whose three vertices have the three relevant colors. Taking their common standard part and applying continuity gives a short proof of Brouwer's fxied-point theorem on the triangle.

But it is well-understood (there's a whole field studying such questions [2]) that the nested interval proof of the Intermediate Value Theorem does not generalize to proving Brouwer's fixed point theorem on the triangle [1]. This fact can be derived from a computability argument as well [3].

Nelson's argument does generalize to prove Brouwer, so it's not the nested intervals argument. But really, nobody cares about these technical reasons. It's obvious to most math undergraduates that Nelson's proof is not the nested interval proof, the clear absence of any nested construction kinda gives it away. The only reason it was necessary to get technical is that you did not really inspect the proof before claiming it was nested intervals. The technical results cited above are just a formal way to show that any correspondence you might imagine between the two proofs is just not there.

[1] Shioji/Tanaka: "Fixed Point Theory in Weak Second-Order Arithmetic", Annals of Pure and Applied Logic v47, pp 167188 (1990).

[2] https://en.wikipedia.org/wiki/Reverse_mathematics

[3] Potgieter: "Computable counter-examples to the Brouwer fixed point theorem", https://arxiv.org/abs/0804.3199 (2008).

> The so-called "nonstandard analysis" hasn't caught on, because it's mostly the exact same arguments wrapped in slightly different language

No. Let's take a nonstandard proof of the intermediate value theorem on [0,1] by Nelson.

By the transfer principle it is enough to prove this for a standard continuous function f on [0,1] with f(0)<0<f(1).

Take a finite subset of [0,1] containing every standard point. Colour its points blue, green, or red according to whether f is negative, zero, or positive at tha point.

The first point of the interval is blue and the last red. Hence either awe can find some green point, or we can find two neighbouring points that have different colours, the first blue and the second red.

In the first case there is a zero, so we are done. In the second, let the neighbouring points be p and q. By the completeness of the real numbers, every nonstandard real in [0,1] is infinitesimally close to exactly one standard real. So p and q are infinitesimally close to some standard real number, let's call it z.

Standard continuous functions send infinitesimally close points to infinitesimally close points. So f(p) and f(q) are both infinitesimally close to f(z). But f(p) is negative and f(q) is positive. The only standard number infinitesimally close to both positive and negative numbers is zero. Thus f(z) is zero. This proves the theorem.

You tell me, which standard proof is this? It's certainly not the nested interval proof. Not the supremum proof. Not the bisection proof in disguise. Which argument does it wrap in slightly different language? Can you point to a single textbook, course note or lecture that gives such an argument?

No. One could of course argue that this is not simpler/shorter than the usual arguments. But it is very different from them. Saying that it's the same arguments repackaged in a different language is just wrong, and detracts from an otherwise valid point.

Now that is a good and interesting question! Hopefully a "no-moatist" will share their reasoning.

That's the ratio the widely published numbers give [1]. One does not have to believe the numbers [2], but those who do believe them are then justified to conclude that there's no moat.

Which numbers you believe is of course going to affect whether you think there's a moat or not. That's largely orthogonal to your TSMC/Samsung analogy I responded to. If you think the "moatists" are wrong because they believe the wrong numbers, that's fine, but then there's no need for the analogy.

[1] https://galileo.ai/blog/llm-model-training-cost

[2] https://medium.com/@theiand/how-can-deepseek-a-5-6-million-l...

No. In the semiconductor industry, the "catch-up" player isn't normally spending less in absolute R&D terms.

Comparing the R&D costs of creating GPT-4o vs. DeepSeek V3 (the latest gen for which we already have good accurate numbers) it looks like the latter cost 1/20th as much to create.

If Samsung could catch up with TSMC for 1/20th of the cost, people definitely would say that TSMC has no moat.

Not for long. Too late to get Business now to exploit this, since EH and the small credit-free Pro allowance will soon be restricted to Premium Seats ($100/m).

If we voice this opinion publicly, the most likely end result is that OpenAI will start billing our chat sessioms against our Codex budget too.

> Maybe it's because I'm American, but I can't imagine actually saying that to someone. I'd sorta expect them to throw hands if I talked like that about Jesus.

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)

> You can tell that Claude really does grasp a wide array of highly specific scientific and mathematical nuances... where's codex is just basically for coding and that's it.

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".

> If it is known that A is provably true then one can study the consequences of A being true

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.

dgacmu: if you're writing C on x64, try AES-128-CTR (AES-NI, 8 way) using the header wmmintrin.h which has hardware accelerated primitives for this. An LLM can implement the RNG for you based on this comment if you want to test it out quickly. It should be faster than PCG, and higher quality.

When was the last time a new PRNG helped you clearly identify a performance bottleneck?

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)

> I’m not sure what point you’re trying to make,

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.

Ah yes, Xorshift, the RANDU [1] of the 21st century [2].

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

> The article was showing the difference between mathematicians and engineers.

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.

Having read the article, I can confirm that it is.

While their math results are impressive, vibe coding their own web UIs with their subpar design models is really going to backfire if their plan is to attract new users with better free model offerings.

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.

I don't think that's it. Multiple or my friends from the target audience (academic mathematicians) admitted to scrolling past because the title made it sound like a review of last month's contributions, instead of 10 new ones.

It looks like Zach Weinersmith predicted this exact line of research 11 years ago [1], when he suggested testing the liar sentence using fMRI.

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

You're confused because the word kernel is used in two different senses.

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.

> . You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions. [..] it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss.

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.

> Really unnecessary levels of snark here. [..] Have you ever heard of prolog?

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.

> The two big discoveries both came from the negligible handful of mathematicians working at OpenAI/Anthropic in spite of many orders of magnitude more mathematicians using them outside of the companies

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.

> This does not sit well with personal experience and I wonder if it is just one of these questions of AI people being unaware of the level of skill that exists in domains they think have been automated.

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.

Going from "current mainstream culture is not perfect" to "there should be more experiments in alternative ways of life" requires the assumption namely, that the average experiment is more likely to improve matters than to make them worse. When these experiments go awry, they hurt not only the participants of the experiment (who are themselves often children or others who have no other choice), but also everyone standing nearby.

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.