Jensen has created more shareholder value than nearly any human on earth.
A) He never made a single product himself, and B) surely we can see in hindsight that this is a pretty goofy metric for success...? Like, "shareholder value" isn't exactly what we need at this pivotal moment in the terran story.
I think the real risk for the economy, the AI industry, and the US is that Nvidia becomes JUST another company.
...
But if this cycle stops and efficiency wins in the market (lower margins, more competitors, more options), then Nvidia goes back to where they were
Even if we accept capital as the most important thing, this seems pretty openly counterintuitive. You're lamenting the spectre of efficiency.
This is demonstrably untrue. Jensen is an engineer through and through, and contributed significantly to Nvidia's early accelerators: from the NV1, at least to the earliest GeForces.
Ha, I was wondering if someone would bring that up! Pretty funny. How much of the shareholder value of NVidia is represented by his share of the NV1 and the earliest GeForces?
> B) surely we can see in hindsight that this is a pretty goofy metric for success...? Like, "shareholder value" isn't exactly what we need at this pivotal moment in the terran story.
In the slow evolution of the human race into the Ferengi, it is absolutely a milestone!
Long term we want efficiency. The market is SUPER inefficient right now. People are buying GPUs and stacking them up in warehouses so that they get their allocation. Companies are taking retired jet engines, and turning them into very expensive generators. SoftBank just defaulted on a bunch of power generation orders (increased cost for everyone, but didn’t create the value). My point is that it will be a painful road to get to the efficient market which will likely be a recession because of a massive slow down in spending
A is a reddit meme-argument. It assumes that the labor-theory-of-value is a fact and implies that only fungible IC's add value, whereas irreplaceable great men who organize multi-trillion-dollar companies from scratch contribute nothing. It's a way for them to advance for their silly worldview while obscuring its absurd foundational assumptions.
Your argument sounds like a satire of itself. Surely it's begging the question to say that CEOs are great men who are irreplaceable and individual contributors are fungible.
Meh, not really. NVidia stock is presumably rebounding as we speak -- unless they pick someone political or unhinged to take over, this will just be a blip.
And I doubt it'll cost him much. What could you pay the founder of the second most valuable company on the planet who already holds $150B in equity? It'd be as absurd as paying Donald Trump.
> NVidia stock is presumably rebounding as we speak
Not in premarket so far, 12% down sing yesterday.
Also why would it do better? Overall Huang seems to be a highly competent CEO. Replacing him with someone seems risky (especially if the board is influenced by Trump & co.). Especially given that Nvidia never had any other CEO.
I guess even if Jensen Huang leaves scorched earth, he will have sufficient money for the rest of his life. On the other hand, any other person who invested into Nvidia stocks will have a much more serious problem. :-)
So, it would not be a dumb idea for Jensen Huang to leave scorched earth and "let the world burn" (and in particular cause utter panic in the AI sector). :-)
Hmm. Which means that they just luckily don't have to prove anything about any software that might halt...? Or?
Like, they use some pretty stark terms here:
Formal verification—mathematically proving code runs correctly without flaws—is the highest standard of security assurance; however, it is difficult and often labor-intensive.
Of course "proving" and "without flaws" are just words in a language game and might not mean the absolute things we expect them to as laypeople. Is that what's going on? Or can the "code" they're "proving... runs correctly" indeed be unrelated to such a fundamental finding of compsci?
I type this message to you all with sadness in my heart, cause I know I could get a better answer 100x faster by just asking an agent to research, which I could then have it dumb down to my level until I grasp it. I don't really know what the point of forums are, anymore. It's undeniably hard not to see ourselves as a planet of sad, fragile monkeys wasting away the hours between birth and death. That was already the case, perhaps, but at least learning and sharing knowledge about engineering in places like this felt like a somewhat meaningful way to positively impact the material conditions of my fellow humans, even in an indirect way. As of November 2026, I'm just the taste/framing component of artificial minds that seem overwhelmingly likely to develop their own within months or maybe years.
For a long time (since noticing the singularity) I've felt like someone doused in napalm and set alight while falling through the sky, frantically trying to put myself out while fixing my broken parachute. But post-Mythos I can't help but fear that there is no solid ground below. Just endless void. :(
Driving a lean proof manually is a lot of effort. It's often 50x or 100x the effort of writing the initial program in the first place. The grand idea here is that if you can get a system to have a good heuristic/intuition for figuring out those proofs, you can lower this effort amplification by a lot. This makes formal verification at this level feasible for mission critical software, and also a larger slew of software we rely on.
The difficulty lies in coming up with the right formulations, and also some times altering the program to make it amenable to proof. It's quite often the case that a proof won't go through unless the program itself has the right idea.
As for the halting problem: it is highly theoretical. Lots of programs which are useful can be proven to halt for instance. Or you can just prove that the program is correct up to the point in time where the sun expansion covers the earth. There are often practical ways around such limitations, including the alteration or reformulation of the program.
Which definition of singularity are you using? I'm still doing my own laundry. It's quite poetic, what you wrote, if a bit sad. The hours between birth and death are waste, but are to be enjoyed. To discover the human condition. Overcome adversity, or die trying. Yes the machine gods will reign supreme but until they come to be, we must play and feel joy and sadness and love, hate... sonder. The planet doesn't have to be a bunch of sad monkeys. Maybe you can make a virus that will turn us into joyous lizards! There is so much left to discover and understand. How do you un-fry an egg?
Formal verification is actually a very interesting concept and topic. There is a famous statement called the Curry–Howard correspondence: every type signature is a theorem, and the implementation is its proof.
So if I have a language where I can encode in the type system that a number is a prime and is even, then for example the following would be a theorem with a proof:
Lemma even-prime: a -> Prime(a) ∧ Even(a) { // read as 'it returns a number `a` that is both prime and even
return 2
}
If we restrict the language enough, we can both encode very complex statements and can make sure that one can only ever write an implementation that compiles if it's actually true. E.g. an ordinary language like python where you could return None instead of 2 would fail these requirements.
So they often have dependent type systems -- in these you can freely mix functions and values in your type signatures, not just types. E.g. you could have a Matrix type with two parameters, and then you can have functions like `transpose: Matrix a b -> Matrix b a`.
---
But this is just one side of the whole thing, the other is how to actually prove anything, like what even is `Even` in the above? A type like `someNum: Int` is also a theorem, but it only translates to "there exists an integer" - hardly interesting.
The real "mind blow" (at least to me) was that we just simply create a type for Equality. It takes the same parameter twice [1] (like in the Matrix example it would be Matrix a a) -- and thus we get a construct that can only be instantiated if the two sides are equal as per the language's compilers rules, that is automatically enforced by the compiler itself!
So now you can have `Eq 2 (1+1)`, but not `Eq 2 (1+3)`. And one last step that makes it general enough for all kinds of proofs, the compiler of these languages are not Turing complete. You can write many things, but for reasoning about loops you usually introduce a fuel that is always decreasing (and thus the compiler will accept it, as it knows it will run out once and that's enough for it). So it can evaluate everything, even in types and creating a normalized expression -- and then accepts everything as equal that normalizes to the same thing.
So for a more complex proof, you can just break down the problem to small steps that are by themselves understandably equal by the compiler.
> Which means that they just luckily don't have to prove anything about any software that might halt...? Or?
the only thing halting problem says is that you can't prove *everything*
feel the difference between "any" and "every"
to stop being able to prove "every" thing you only need to 1 counterexample - which Turing found
all explicit examples of unprovable things are very removed from real demand (other than "prove arbitrary program halts", which probably doesn't count as real demand anyway and more of vapordream)
Wow, fascinating! I hope I’m not the only OCR-minded soul on here that immediately started thinking of pipelines for this one could assemble from all our new DL-enabled toys… it’s a shame that “some American kid” probably doesn’t meet their contracting requirements.
One thing that kinda baffles is that it sounds like the snippets (I bet that German word is fun) haven’t been scanned(/photographed…?) yet. No matter who they contract with, wouldn’t that necessarily be step #1? Or is the scanning the part that needs contracting, and the “e-Puzzler” name was just a lil melodramatic?
For one thing, I feel like it’ll be wildly helpful that they’re on a variety of papers, not challenging like they imply. Once that and bag index have narrowed down neighbor candidates, you’ve got rules and glyphs to go off of, much less recognizable form layouts. It feels like the Vesuvius scrolls but actually tractable…
Sorry, I didn't mean to imply it was trivial, but rather that it's necessary if they are to make any progress at all. I mean, right? How could one assemble a puzzle without being able to perceive the pieces?
16k bags with 3k shreds each is a few million pieces. You could scan 10-20, or more, at a time spreading a them over a glass sheet, putting other on top and making two pictures. Have a few people doing that and you can process a bag in a few hours. 16k bags for a team that can process 10 bags in parallel is like a year of work.
After that I bet the full reconstruction takes like a month tops with AI matching pieces.
It helps that they used bags; because if all snippets were in one bag, then combinatorially, things would be much more difficult.
n pieces residing in the same b_i, i<16501 bags can be viewed as a blocking function in record linkage. That means while comparisons are O(N^2), here N=16500 and not N=i*16500. In practice, filtering by compatible color (effectively a 2nd-level blocking function) prunes the search space further.
The simplifying heuristic (works not always, but most of the time): "assume that all snippets belong to the same bag".
One important question is how big the individual snippets are - ideally, they'd contain fractions of more than one line of text on top of each other.
According to @Pebblebox (see below), “Each bag contains between 2,500 and 3,500 fragments of torn-up pages.”, which means the fragments must be large enough on average to be amenable to language model application.
Then I'd create a data structure with the color of a snippet and its lines of text (either full lines, or prefixes and suffixes at the [left/right] fringes):
type snippet_type = record
snippet_color: RGBColor;
text_height: integer;
text: lines[1..5] of record
left: string;
right: string
end
end;
A statistical or neural language model should be able to piece individual pieces together and come up with a list (sorted by likelihood) of locally probable solutions (called "trellis" or "sausage" in ASR parlance), which can be combined using a beam search.
That’s an odd price. Not knowing what a “bag” means, I think 13-gallon (“kitchen”) or larger lawn clippings bag is possible.
I wouldn’t for €100 sign up to scan even an office wastebasket (6-8 gallon) bag of torn-up paper. Make it €2000 for that quantity, and we’ll start talking.
I worked in the Pentagon from 1989-1995. I handled “burn bags”, among the other classified stuff I did.
I can’t speak for what their bags are like, but ours were basically large, thick, grocery-size paper bags without handles. Thick enough that they most likely wouldn’t tear, even if they were full and mid-handled somewhat. You rolled down the top and stapled them shut.
But we didn’t shred our documents first. We just put in whole sheets and reams of paper, and we left it up to them to shred first and then burn. But then, that was 1989.
Well that seems like problem #1, then. One is a data science/applied ML task, and the other is a large-scale, human-labor-intensive process; the best company for the latter would probably be some sort of bespoke machinery producer from the food industry, TBH.
Very well-written, and undeniably relatable! Sadly, I am compelled by forces beyond my cognitive control to respond, especially to points I've seen and refuted before. If nothing else, I hope it's helpful to know the other side of these things :)
using LLMs in my codings
I hope it's not too combative to start by saying this is a huge red flag for someone who hasn't checked in on what post-Mythos agentic engineering is like. Of course LLMs are undeniably involved, but it comes off like someone quitting social media by decrying protocols (or worse: series of tubes). LLMs are an essential component that has finally thawed the AI Winter, yes, but they're still just parts of a system. A harness is far from a mere wrapper around a neural network, to say the least.
people argue that "LLMs are just a tool", but really, it is not, it is a SERVICE
That dichotomy is a false one (many software tools are productionized as services), but the underlying sentiment is clear and common: that querying a chatbot is akin to asking another human to do something for you. This comes up most often in Reddit's vicious "AI wars" about digital art, where generating an image cannot be a creative act on the users' part because it's more like comissioning a painter than it is like painting.
I think the response is obvious (and why this is merely an aside rather than a "dealbreaker" proper): this is granting personhood to neural networks, which no one who supports this point would admit to in a thousand years. Either they're people and you're asking a person to think/paint for you, or they're inanimate machines and it's a tool; there is no middle ground. (If unconvinced: what about a camera makes it a tool to be used rather than a peer to be delegated to? It can draw a picture in milliseconds!)
the current hype and craze for them
This is an underlying worlview thing that poisons the rest of the analysis, namely that nothing (important) ever happens. That surely this just a hype moment that will pass like the iPhone moment and the Bitcoin moment, and that anyone who says otherwise is surely crazy. It's begging the whole discussion.
And it's no wonder, there have been several studies confirming this:
The first paper is Microsoft's[1] recent incredibly informal survey of how people feel working in a career they know to be changing beyond their recognition, and with tools that didn't really exist 6 months ago. Yes, orchestrating agents is a different experience than we're used to; no, a simple survey could never prove that they are cognitively dangerous.
The second paper is notoriously misleading, and a stain upon MIT -- observing brain activity differences between people who have to think deeply and write an essay by hand and people who type a sentence and then sit there until the allotted time is over is not surprising, and definitely doesn't show what they clearly intended the flashy graphics and suggestive conclusion to show (that using chatbots leads to brain damage). There's more, but long story short: they're manipulating valid techniques to make a tool seem like a uniquely-dangerous toxin, when the exact same effect applies to all previous tools of note (calculators, typewriters, word processors, translators, even Grammarly).
The third paper is just highly-speculative, deeply-polemic schlock, obviously.
The quality of the output is not that great
1. This is an unfalsifiable claim, which is lucky because the goalposts have had to be moved many times to get to "looks impressive, but is sometimes complete bullshit". Turing refutes this thinking quite directly in `§6.5` of Computing Machinery and Intelligence (CMaI)[2].
2. Many experienced engineers disagree, to say the least, as do companies investing billions.
3. Again, you can't help but sense the author hasn't used post-Mythos models; even if they have, the fact that such a huge leap has occured in just the previous 24 months is overwhelming evidence against this notion. The linked sources being A) an /r/AntiAI post (!) and B) a pre-Mythos essay don't help.
Congratulations, you have let OpenAI/Anthropic/Elon Musk dictate what your code does and why.
I'm quickly getting the sense that the author is too vitriolic and dug in to be reasoned out of these views :( Hopefully it goes without saying that "your code sucks because you gave it to [HATED_FIGURE]!" is an invective, not a premise. For the rest: see previously preceeding section, which is indeed "closely related".
I like writing code
Same! I also like playing video games and tending to plants -- just had a blast on Beyond All Reason last night, and my Philodendron Florida Ghost just unfurled a wonderfully-ghostly new leaf. Neither are my career.
Environmental aspect
I'm most dissapointed by this part, as this person is Finnish and should know better about the Google story :( What's being framed as some unheard-of act of environmental terror is really just the planned and almost-completely-permitted early harvest of a small plot of "planted forest", i.e. a tree farm, which are one of Finland's main industries. Everything in this map in blue is tree farms, with the Muhos site in the middle: https://i.imgur.com/HyTVp1I.jpeg [3]
The preceeding 'this technology uses power' point doesn't need refutation, but it underlines the problem with the point above: this is post-hoc reasoning. Cutting down a tree farm in Finland is so, so far down the list of priorities for actual environmental activism that it's hard to describe, and yet this post has nothing about not working for companies that serve non-vegan meals for lunch, uses air conditioning, or flies people to yearly retreats.
But I just personally feel squeamish about having my work being done by rather skeezy companies
Even if this were relevant (which it's not in a post-GLM-5.3 world[3]) it offers no argument, and thus cannot support the conclusion.
Even if some technology or tool sticks around, it does not necessarily mean its good idea to work with it.
Also not an argument. Heroin isn't inadvisable because it's "here to stay", but rather because it's a toxic, extremely chemically addictive narcotic that kills many thousands of well-intentioned users every year, and ruins thousands more families before that.
TL;DR: Apologies to the (again, clear & well-intentioned) author, but this essay is like heroin -- I dislike it!
---
[1]: BTW, there's a reason Microsoft published this, and it's the opposite bias that this author assumed. Read this article and see how deep the conflict of interest admission is buried -- it says it all: https://www.project-syndicate.org/onpoint/anthropic-training...
Which is why none of us have or want job titles with "programmer" in them; even juniors are junior software engineers. As long as a human is needed to design and implement good software, they will be software engineers. The temporal affordances aren't nearly as unique as you imply, either: generated code and unit test results are two good examples of things that "keep going... much like a motorized machine".
That is, unless you treat the agents as if they were people and thus the true engineers, of course. I think that's a fascinating philosophical topic despite ultimately disagreeing, but to say the least it's incredibly controversial to even consider the personhood of agents, much less endorse it.
This is all moot anyway, so apologies if I'm rude or overly dismissive of your comment that I agree with the general thrust of. No point starting fights over deck chairs...
reply