formele verificatie
Axiom laat AI-agents het grootste wiskundebewijs controleren
Axiom zette de classificatie van eindige enkelvoudige groepen (15.000 pagina’s) in 24 dagen om naar Lean, met 43,1 miljoen regels code en tientallen AI-agents.
Claude bewijst wiskundig dat 123 codebibliotheken niet crashen
Anthropic liet Claude formele bewijzen schrijven voor 123 opensourcebibliotheken. Daarbij kwamen honderden bugs boven, sommige meer dan tien jaar oud.
Wiskundigen wegen AI-bewijs van GPT-5.6 Sol Ultra
Het bewijs dat GPT-5.6 Sol Ultra leverde voor een 50 jaar oud grafentheorie-vermoeden ligt onder de loep. Wiskundige Thomas Bloom prijst het maar mist bronvermelding, en formele Lean-controle ontbreekt nog.
Leanstral 1.5 van Mistral vindt bugs met wiskundig bewijs
Mistral geeft Leanstral 1.5 vrij, een open Lean 4-model voor formele verificatie dat 100 procent haalt op miniF2F en vijf onbekende bugs vond in open-source code.
AI helpt Fermats laatste stelling te formaliseren
Wiskundigen aan Imperial College testen AI om delen van Fermats laatste stelling in Lean te formaliseren. Wat autoformalisatie is en hoe snel het gaat.