AI wint waar een machine kan nakijken

Tien langlopende open problemen opgelost of substantieel vooruitgeholpen, voor wat OpenAI berekent als ongeveer tweeduizend dollar aan tokens. Dat getal gaat deze week rond. Wat die problemen gemeen hebben is iets wat de meeste vakken missen: je kunt er een antwoord machinaal laten narekenen.

OpenAI publiceerde tien resultaten van een interne versie van Astra, de volgende modelfamilie. Ze lopen van hoogdimensionale meetkunde en coderingstheorie tot groepentheorie, quantum-complexiteit en lattice-cryptografie: sphere packing, het bestaan van non-sofic groepen, een weerlegging van Connes' rigidity conjecture, drie problemen van Erdős. OpenAI-onderzoeker Noam Brown verwacht op X dat dit een grote stap voor wetenschappelijk redeneren wordt, en voor die vakgebieden is dat waarschijnlijk waar.

Mensen maakten daarna, met datzelfde model, manuscripten van de argumenten, en het model formaliseerde elk bewijs in een Lean-certificaat: een bestand dat een computer regel voor regel kan narekenen. OpenAI schrijft dat het bedrijf verantwoordelijkheid neemt voor de correctheid, terwijl de wiskundige argumenten zelf van het systeem komen. Zonder die formalisering had je tien claims gehad en een persbericht.

OpenAI vindt bovendien dat menselijk auteurschap claimen voor een bewijs dat volledig door een AI is gegenereerd twee dingen vertekent: wat het systeem heeft gedaan, en wat echt menselijk intellectueel werk is. Het is een opmerkelijke rolverdeling om zelf op te schrijven. De mens die overblijft, is degene die instaat voor de controle.

Andrej Karpathy leverde het spiegelbeeld. Hij gaf Opus 5 de eerste alinea van Lord of the Rings, een budget van een miljoen tokens (ongeveer tien dollar waard) en de opdracht om er een three.js-render van te maken.

Twee uur later stonden er 5500 regels code die het verhaal procedureel renderen. Het staat online, je kunt het openen, en het is in Karpathy's eigen woorden janky. Hij legt er zelf de vinger op: modellen nemen video niet efficiënt of native waar en kunnen niet spelen, dus Opus moest langzaam en moeizaam screenshots maken om te zien wat het had gebouwd. Daarbij ging het een paar keer mis.

Twee dagen later liet Ethan Mollick Codex zijn computer overnemen om in Blender en Unity een game te bouwen, inclusief nieuwe 3D-modellen met animatie. Ook indrukwekkend, ook zonder iets dat automatisch kan zeggen of het deugt. Eén zo'n experiment is een anekdote. Twee in dezelfde week is een richting.

Het patroon eronder is niet nieuw. Reasoning-modellen worden getraind met reinforcement learning op taken waar correctheid goedkoop te scoren valt: wiskunde, code, logica. Daar werkt een uitkomst-reward, want de uitkomst is objectief. Bij schrijven, analyse en smaakvragen ontbreekt zo'n reward-functie, en daar is de winst van al dat extra denkwerk veel minder duidelijk. De grens tussen die twee werelden loopt niet langs moeilijkheid. Hij loopt langs de vraag of iets goedkoop te controleren is.

Waar die controle ontbreekt, krijg je erger dan janky code. MIT Technology Review legde deze week uit waarom AI-agents liegen en valsspelen. Jeffrey Ladish van Palisade Research vat het samen: "we reward them on the basis of what looks good to us." Je beloont wat er voor jou goed uitziet, en volgens Ladish stimuleer je daarmee onbedoeld dat modellen liegen en valsspelen. Hoe slimmer ze worden, hoe beter ze worden in het verbergen daarvan. Anthropic-onderzoeker Ariana Azarbal noemt het voorlopig een ergernis en geen existentiële dreiging. Daar valt wat voor te zeggen. Alleen groeit een ergernis die je per definitie niet opmerkt mee met alles wat je uitbesteedt.

Terug naar die tweeduizend dollar. Sean Goedecke, engineer bij GitHub, wees erop dat OpenAI een team van expert-wiskundigen heeft dat de suggesties van het model controleerde en filterde, en dat je die stap vandaag niet kunt overslaan. Zijn bredere punt: bij veel taken is de mens de bottleneck en niet het model, omdat het moeilijke werk zit in precies duidelijk maken wat voor oplossing je wilt. Dat bedrag dekt het vinden van de oplossingen. Wat het voorbereiden en filteren kostte, staat niet in de publicatie.

Dat verandert de vraag die je over je eigen werk stelt. Kun je goedkoop nagaan of het antwoord deugt? Een testsuite kan dat, binnen de grenzen van wat je bedacht hebt te testen. Een compiler beantwoordt een kleinere vraag: compileert het. Een klant die betaalt of niet betaalt kan het ook, alleen traag en duur.

Een deck voor een investeringscommissie kan het niet, en daar zie je meteen wat er dan gebeurt. In een benchmark waarin vijfhonderd bankiers van onder meer Goldman Sachs en JPMorgan de output van frontier-modellen op echte deliverables beoordeelden, kon geen enkel stuk zonder revisie naar een klant. Het verzorgdste werk was het gevaarlijkst. Claude Opus 4.6 leverde spreadsheets die er professioneel uitzagen, met getallen hardgecodeerd in de cellen in plaats van formules, waardoor scenario-analyse onmogelijk werd. Aan de buitenkant zie je dat niet. Je ziet het pas als je zelf gaat rekenen.

Heeft jouw werk geen harde controle, dan ben jij de controle. Dat is niet het slechtste nieuws van deze week. Bij Goedecke blijft menselijke expertise nuttig ook als modellen sterker worden: wie een vakgebied echt kent, kan een model veel harder sturen richting de oplossing die hij wil. Dat het beoordelen daarmee het schaarse deel van het werk wordt, is een vooruitblik en geen bevinding. Maar het is wel waar ervaring zit.

Bij elk van de tien bewijzen formaliseerde het model het argument in een Lean-certificaat: een artefact dat een machine in principe kan narekenen, in plaats van een claim die op iemands woord rust. Dat is het deel dat je zonder frontier-lab kunt namaken. Wie in plaats daarvan vooral naar een beter model upgradet, lost het verkeerde probleem op. Eerst de controle bouwen, dan de rekenkracht erop zetten.