While Paramount claims they cancelled Colbert as a cost cutting move, that makes no sense since other late night shows on other networks with smaller audiences continue. They must make some sort of financial sense.

It is widely understood, though not provable, that the move was a bribe to Trump in order to get the merger approved. Trump has had a longstanding dislike of Colbert because of his commentary on Trump as a person and as the President.

When is a hard question. Rationally it should never have blown up this much in the first place (some expansion would be rational, but not like we've seen). Clearly the minds driving this are not rational.

Insanity is notoriously hard to predict. That's why short selling is so risky. The market can clearly remain irrational longer than most people can remain solvent when betting against it.

Good question. Their POWER series of CPUs were not insignificant in capability, their chip designers were clearly technically sophisticated, and GPUs are just specialised vector processors with a few extra bells and whistles - stuff IBM is extremely familiar with.

It would not have been difficult to release a GPU or other LLM-specific processor to go along with the POWER11. They'd been working on the POWER11 for 4 years, they knew in 2020 that LLMs had a strong potential to be significant for Big Data processing - an area you use big iron for, they're not rank amateurs, they have plenty of reserve, they could have assembled an emergency team to build a vector processor that was custom-designed for just LLM work, and released an LLM processor card that could run circles around nVidia.

They didn't. Because, as has happened before, their management is simply too stupid and too slow.

They can work, but they have major issues.

1)For at least the first 6 months, if not the first several years, it will take more time and money to teach them than they generate. Why would any company do this?

2)As a hiring manager at company B, I see you apprenticed at company A. I have no idea if that means you're qualified. I can't trust company A to tell me, they're a competitor. Schools stand as a neutral 3rd party telling me that they've completed a set curriculum and should know that much. It's not perfect, but it's a start.

3)Some fields just have a huge amount of up front learning before you can be useful at all. Apprentice plumber? You can run and fetch tools and hold things in place while you watch and learn. Apprentice electrical engineer? You have no idea what inductance is on day one. There's literally nothing you can do. So basically at this point you're hoping the company sets up a school.

I meet them all the time. Most of them are in their 50s and have used computers their entire adult life.

I don't want to diminish the accomplishment; that seems like a very cool dataset and probably one that was really fiddly to pull together; but, if you are talking single-neuron resolution; I am curious about whether you can still call an individual sample "the human brainstem" rather than "a human brainstem" and what comparative purposes you can use it for without running into trouble with cases where there are multiple ways for a brainstem to be adequately healthy, so long as certain requirements are met, so you'll need considerably more samples to draw useful inferences about exactly what the problem abnormality is.

Same sort of thing as when "sequencing the human genome" was a big project. Obviously a major exercise in gene sequencing and a basis for situating subsequent sequencing operations; but once you start talking detail there isn't 'the human genome'; literally everyone has one; and it turns out that different differences matter or don't at radically different levels.

Presumably the methods used to do it once will be helpful in doing it more often in the future; but I'll be curious what we discover about the balance of 'normalcy' vs. some relatively subtle and confusing combination of surprisingly variable ways to have a brainstem that seems to work just fine along with surprisingly subtle, no ghastly big lesions, ways to have one that ends up being totally dodgy.

I find "NOTE: Experiences vary by region." to be a bad sign for something that would be so trivial for MS to alter the behavior of; and where they are obviously not earnestly making improvements that were previously impossible but grudgingly rolling back bullshit they thought they could get away with.

Probably means good news for users in the EU; same way they get left out of some of the most egregiously bullshit 'AI' stuff; may help EDU and enterprise; but I'm guessing that it's no promises for less favored users.

Or let's put this another way. Show of hands - how many of you "spicy autocorrect" / "stochastic parrot" people had "AI will start mass-solving Erdos problems" on your forecast list a couple years back? Huh, none of you? Fascinating!

Take some time to reassess your priors. And while you do so, understand that, yes, they are doing logic / reasoning.

They weren't discovered by an LLM. They were known conjectures that were proven by an automated solving language that was linked to an LLM.

I'll take "Things That Didn't Happen For $200", Alex.

Only a handful of meaningful proofs have ever been done by automated formal theorem solvers (the Four Colour Theorem being the most noteworthy example - but its proof is so long that humans can't verify it). By contrast, AI tools have been solving Erdos problems en masse. The majority of them just bog-standard commercial models. In case you need help, the only ones on that list that were hybrid (AI / non-AI) in the actual solving phase are:

1) AlphaProof / DeepMind Prover Agent / AlphaProof Nexus
2) Aristotle (Harmonic)
3) Seed Prover / Seed Prover 1.5 (ByteDance)
4) AxiomProver (Axiom Math)

In each of the above, LLMs come up with the lemmas / strategies but then use Monte Carlo search ("brute force") or likewise to investigate what they came up with. These are a minority. In the "AI Standalone" category, these "hybrid" tools made up only ~20% of attempts and successful proofs. Hybrid tools actually made more of a contribution in the "AI Alongside Literature" (related literature found afterward) and even more of the "AI Building On Literature" (related literature known beforehand) categories, which is the opposite of what people like you expect.

And even with the hybrid tools, it's still the AI doing the heavy lifting when it comes to strategy. Non-AI theorem solvers, again, don't have a spectacular record for churning out novel proofs to unsolved problems. Tools like Lean are more about mathematical rigour - a passive environment that requires a driver (a human or AI) to feed it actual strategies, lemmas, and proof steps. And no, you cannot brute force "strategy" in the vast majority of cases, which is, again, why automated theorem solvers don't have much of a track record with unsolved mathematical problems.

Let's take a random example: the disproof of the unit distance conjecture. It was solved purely by a general purpose commercial GPT model, not custom-trained to mathematics, with no external tools. Read what the various mathematicians reviewing / commenting on it have to say (sections #3 and onward). Seriously, don't skip reading them, actually read them. This was one of Erdos's favourite problems. He mentioned it commonly in his lectures. Essentially every mathematician working in complex geometry has thought about this problem. The approach that the model came up with was highly novel approach, based on CM-fields and class field towers.

I know you don't want to accept this reality, but it is the reality, so you better improve your ability to accept it,. The field of mathematics is already doing so.

Dang, link didn't post.

Ah, good 'ol "Model Collapse" theory that people have been pounding on for years now, predicting an imminent collapse in model capabilities. How has that been working out for you?

Except what the US is actually facing, at least in the near term, is just the opposite, a worker shortage.

You can't pay royalties to the entire internet. That's not realistic.

What is practical are things like taxes to fund public benefits, or requirements of returning things to the commons (for example, open models).

What if...

Someone (say someone who was familiar with doxygen and GCC) developed number of comment types, where some stipulated preconditions that must be true for the function to run correctly, postconditions that must be true once the function has run, kernel facilities that the function definitely needs, and kernel facilities that the function definitely doesn't need. These would all be optional for any given function.

A static checker could then validate if the code meets the behaviour expected by the programmer. This is precisely what is done in SPARK, a fork of Ada for high-reliability code. Combined with existing static checker capabilities, this would greatly increase the number of bugs that could be caught with all kinds of tools, AI included.

It could ALSO build a full fine-grained mapping for any fine-grained mandatory access controls system. You'd also want includes that you could import for precompiled libraries. This would allow someone to verify if the code was making unanticipated/undesirable calls but would also make SELinux possible to develop for at the application level.

It would not be trivial. If it was trivial, it would have been done simply because it already IS done in other languages and that makes it "obvious" to anyone who has been programming for a while. However, it should not be massively complicated, simply because you can use AI as the static checker. Once it has a definite set of bounda that must be satisfied, it should be much more capable of knowing what paths would violate those bounds. Which means that the checker stage essentially is trivial today, leaving only the markup stage.

You're the one making the claim that modern frontier models still make this mistake (they don't), so how about you go to a frontier model, reproduce what you're claiming happens, and click the "share" button and post the link here?

Don't worry, I'll wait.