saithound

> Cheaper per line of code, maybe.

Cheaper as in the customer who wants to _buy_ software is not willing to pay a high price for it.

It might become a massive problem for the people who use AI to _sell_ software, I don't think we disagree on that.

Well, I don't think we disagree. It might turn into a Bertrand market instead of a Cournot one in China. That just means the end consumers capture the benefits, though.

This is a rehash of an age-old complaint: "I shouldn't have to pay taxes for things I don't personally want or need". A lot of people made that argument, and it does not seem to resonate with the voters. You're naively hoping that AI has finally made it compelling. I wouldn't hold my breath.

You may even be right that a lot of academic prose is suddenly cheap. But just think about the hardest cases of self-justification in academia: classics or literature. These don't promise your hypothetical plumber anything. It's not like he'll ever read a classics journal. People have made your exact arguments against them for half a century, and these departments are still funded. Heck, when "I'd rather give my money to Hollywood" couldn't even defund film studies, "the AI can write a passable essay" has little hope of defunding academia in general.

You could hire a PhD student or tutor to write you an essay or answer your questioms way before Fable 5.1, but hypothetical plumbers cared little either way, so the public commitment to university funding is not about whether plumbers can get the outputs somewhere else.

The government funds academia for the institutions themselves, and the voters who depend on the institutions are not fringe. In many US states the university system is among the largest employers, a huge share of voters are alumni or parents of students, or business owners who depend on selling food on campus, etc. Their stake is high, they're willing to vote on it: the hypothetical plumer's stake is a few marginal dollars which he won't even get since the budget will allocate it elsewhere, on some other service he probably doesn't use. And he doesn't read journal content eiter way. So you'll keep paying your fair share for it, because it's up to the voters, and they care little for what you personally want.

If mainstream corporate America thought it would turn increasingly cheap intelligence into higher revenue growth and higher profit margins, then mainstream corporate America needs to go back to school.

If you want to increase your profit margins, you'll have to innovate! Adopting AI tools that somebody else created, and are equally available to your competitors, won't increase your revenue or margins. The ones who will see increased revenue and profit margins are the ones who actually innovated, by creating the AI.

This is exactly what Apollo reports: the Magnificent Seven increased their profit margins, while mainstream corporate America didn't.

Indeed, they are doing this, just slowly and strategically, to not turn off the knowledge tap. A major company I do some consulting for just migrated from Figma... to Anthropic Claude.

Agered. These are essentially numerology models.

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