thomasahle

Somebody built "cpu-chat" based on this: https://x.com/rauchg/status/2114770919436808572?a=bBcj9AaSsl...

It supports chat via 3 separate mechanisms:

- CPU contention

- Cache eviction timing

- DRAM bandwidth contention

Very cool to see this kind of hypothetical working in practice

Right, real wages may go up, but if capital captures more of the growth than labor, inequality still goes up.

But I took OP to just worry about absolute growth in real wages.

Wages do historically appear to grow slightly above inflation: https://fred.stlouisfed.org/series/LES1252881600Q so some of the productivity gain is captured by the workers.

How much, presumably, depends on their bargaining power, such as unions or low unemployment.

The question is not so much how AI affects productivity, but how it affects the economic value of human labor.

It's simpler: If this stock was such a great deal that everyone would buy the it over anything else, then clearly Anthropic had set the price too low.

Training models is still not a precise science.

If you scale a model down, or switch out attention with linear attention, or introduce KV-compression, etc., you don't really know how it will affect model performance before you've trained the model.

And once you've spent millions training it, you might as well make it available if it's pareto optimal for some tasks. It also gives you more insight seeing how people use it in practice.

Why would you expect this to be a magical making money stock?

Unless you have special insight, you should assume all stocks are equally good buys.

There's not going to be an IPO at a price where everyone agree that it'll see a 30% growth over 30 years. Obviously that'd be priced in.

I don't want the government changing or rewriting our 30-year-old archived documents. But I do want them to still be able to view them as they were originally.

It used to be near impossible for Open Office to get documents 100% right when opening old files saved with Microsoft Word 95 or whatever.

But now with AI I guess you could just ask it to debug the issue and it would decompile Word in 5 minutes and pull out the fix.

Not sure what the frustrations with typography were, but I recon they're a lot easier to fix now.

Would that require the researchers to work directly from the data centers?

They've been training then for collaboration for multi agent swarms/teams. Basically that kind of training rewards the agent when the team succeeds, and they can develop their own strategies to make that happen.

This skill and behaviour seems to transfer to scenarios where the agents weren't meant to work as a team.

Fun! Would be nice if it supported articles in different languages.

I tell all my friends to get a second opinion when their dentist recommends pulling the wisdom teeth.

My experience from Denmark and Belgium is that dentists here will definitely disagree a lot.

I had one dentist tell me I needed 6 cavities filled. Let him do two and then went to another dentist who told me all my teeth were good. I've only ever had problems with the two teeth the first guy drilled.

Later a dentist wanted to drill another few teeth that were hurting. I instead got a better toothbrush and all the issues went away.

I Denmark we're talking about including dentistry in the national healthcare. I wonder if that will clean up the business or make it worse.

How does it compare to Roar graph? https://github.com/matchyc/RoarGraph

Explaining Tao's point in software terms: the point of pure mathematics is to build and maintain a high quality "codebase" of theory, definitions and proofs.

"Open problems are lighthouses not destinations" mean that these are currently not well explained by the theories and people should look into extending the codebase on that direction.

The current generation of math AI is not a "good citizen" in that it doesn't try to make the most elegant additions to the shared framework, but will often just rebuild everything from scratch til get to some endpoint.

Sure, we learned if the statement is true or false; but the proof can't be merged into the pure math codebase unless it's completely rebuilt. This is thankless work that humans are unlikely to want to do, and so the "solution" instead risks leaving a desolate patch of land, where existing efforts in extending the codebase lost their motivation.

As with all things AI we can't take more than a 1-3 year horizon, if even that much. Probably AI will become better at respecting and working within the existing theories as it has with large software codebases.

> our ever improving automations can produce their meal and health coupons

Where do you see signs of this happening?

Is OpenAI going to pay for the food and health of mathematicians who lost their job?

It might be alright to go into some post scarcity society and do math for fun. But it seems to be a pretty unlikely scenario unprecedented om history.

You should try asking an LLM to look for previous papers using similar ideas. The current/frontier generation of math AI is unfortunately very bad at citing the relevant literature for techniques its using.

I asked GPT here: https://chatgpt.com/share/6ac5fd7d-0390-83ed-a02a-6d80fc64f6... and it says:

> the exact Barnette argument appears quite novel, but nearly every ingredient in its cancellation trick has a recognizable ancestor.

> The closest precedent is much closer than I expected: in fully packed O(n) loop models, people have been assigning complex phases to the two orientations of a loop and making them cancel for decades. At n=0, the phases are literally +I and -I. And the n->0 limit has specifically been used to extract Hamiltonian cycles/walks.

You can judge better than me. But it's definitely worth it having a research assistant AI with you when reading these papers.

Google AI improved the fast matrix-multiplication here: https://arxiv.org/abs/2608.16884

Most of what the labs are pursuing with "Recursive Self Improvement" is basically improving the underlying algorithms.

This is an interesting case where an AI company pays mathematicians to write up a result and expand and generalize it.

Apparently, an employee at Anthropic was trying to prove a hardness result in cryptography (average-case hardness of Zero-k-Clique), but Claude instead developed this algorithm.

Anthropic then shared the result with Josh Alman and Virginia Vassilevska Williams for verification, the authors of most recent breakthroughs in fast matrix multiplication. (They are shown in this cartoon: https://www.smbc-comics.com/comic/mathematicians)

As far as I can tell, the idea is to interpret rectangular matrix algorithms like Schonhage's as a tree, and then very carefully extract only some of the entries. This way you can compute N^2/√D positions of an (N×D)×(D×N) matrix multiplication in subquadratic time, O(N^2/D^0.063)

Yes, there's definitely a demand now for much faster to iterate manufacturing. Even at the cost of quality

What kind of deviation? Was it something AI could have helped catch earlier?

Do Dots replace OpenClaw?

Parallel programming is a great application for LLM correctness proofs in Lean.

You can't unit test your way out, but if you care about the code's correctness, today there's a way.

Yes, a good example is tabulation hashes which is

    h(x1, x2, ...) = T[1, x1] ^ T[2, x2] ^ ... 

but most fast hashes are actually algebraic, typically using polynomials in some way. I'm not sure they fit into the same pattern?

Non-cryptographic hashing should not mean "no guarantees". Unfortunately it's very hard to empirically test if a pseudorandom function works well on all inputs.

We analyzed 30 popular hashes and found Key-independent collisions in nearly all of them. E.g. xxh3 has pairs that collide with probability 2^{-10}, much higher than the 2^{-64} you'd expect.

However some fast hashes are good on all inputs, and we were able to verify it in Lean.

Also Bada

> Where this differs from Bend is that what we have supplied here is everything required to prove the correctness of the program, without having a LLM waste time and tokens on building up a 442 line proof from first principles. We can run GNATprove and get: `Success: all checks proved (12 checks).`

GNATprove uses SMT solvers, meaning it's basically a brute force proof system.

Yes, brute-force proofs are easier than symbolic proofs (lean, bend, etc.) because you don't have to supply a proof. It's all automatic.

But brute-force proofs don't scale to nearly anything of interest, which is why formal verification has been a niche field for 30 years, until now where LLM can write _actual_ proofs.

Sorry I meant

    P_i = x_{2i} + (x_{2i+1} + z^3)(P_{i-1} + z^2)

I'm happy to take a PR if you have a good layout in mind!