Saturday Links: AI Economics, Theorem Proving, and AI Remaking the Software Stack
AI Economics, Theorem Proving, and AI Remaking the Software Stack

Here are this week's links:
- Tech tycoons have got the economics of AI wrong. I generally love The Economist, and on AI, they have generally had good takes. In this article, I think they miss the point entirely. The Economist argues rightly that all the invocations of Jevon's Paradox (where making something cheaper makes us use more of that thing) by tech company CEOs are annoying, but also very probably wrongly that it likely won't apply to AI. I think even in late January (when this was written), it was already abundantly clear that AI has utility layered into almost any information workflow. More processing, more automation. and an almost inevitable acceleration of use not just of AI but of all compute. In Microsoft's latest earnings, for example, it was general compute growth that gave the biggest lift to their numbers.
- DeepSeek-Prover-V2: Meet the New Addition to the DeepSeek Family. The sequence has an overview post of work on a DeepSeek variant based on mathematical theorem proving. There is still quite a way to go to beat human benchmarks but it's exciting to see new training methods that focus on problem decomposition. It seems unlikely to me that a pure LLM model will exceed human capacity any time soon, but a general LLM + a theorem trained LLM + some kind of mathematical execution environment like Wolfram Alpha seems like it could get there and beyond at some point.
- How Good Is ChatGPT at Giving Life Advice, Really? Getting life advice has rapidly become one of the top use cases for AI chatbots. That leads to the natural question of – is it actually any good for that? Short answer from the small study: actually, it's not bad at all across quite a few query types. I'm not sure if that's a relief or a worry. I guess a relief that since people will clearly use chat bots this way, at least the best don't completely suck. Worry that the failure modes will probably be subtle and may even change human behaviour. The recent extreme user-pandering ChatGPT engaged in could lead to very bad outcomes. More worryingly, it's clear that users can quickly become attached and even dependent on AI interactions. A few studies are starting to show complex relationships between chatbot use and human well-being factors such as loneliness.
- 1,000 AI-Enhanced Works Now Protected by US Copyright Law. US Copyright is clearly allowing AI-enhanced work to be copyrighted (whereas purely AI-generated work cannot be). The test revolves around whether "creative choice" was automated through AI, or whether this was still driven by a human creator. This seems an eminently slippery slope to me. How long does a prompt need to be? How many post-generation edits are required? Much of the ire of Artists about AI copyright violations is actually about image generators being trained with human-created work, which is a different but related issue. If an AI-enhanced work can be copyrighted, should the decision take into account whether the enhancement was done using a tool that itself might be considered to be violating copyright?
- The Hyperspace Bypass. (Thanks to Sam Ramji for highlighting this.) With the rapid change in AI capabilities, it's sometimes easy to miss the big picture. In this article, Stephen Hood does a great job of stepping back and framing what AI is likely to do to applications and the compute stack. The past 30+ years have built layers and layers of capability and abstraction from the chip up to the app. Each layer gave us more capabilities, but it also imposed more constraints and patterns. AI changes our ability to create everything from workflows to UI in a new way, potentially bypassing or remaking many of those layers (hence the bypass). A user with an AI assistant can potentially navigate, aggregate, control, and visualize a lot more information (and IT-controlled systems) than they can with a phone full, or apps or a web browser. It's still unclear whether this will emerge as an open ecosystem like the early HTML web did, or a set of closed silos. Hopefully it'll be the former, but there is a lot of work to do to make that happen! (The article goes over some of the key challenges.)
Wishing you all a great weekend!