Lean
Anthropic-model bewijst quantumvermoeden uit 2008
AI-bedrijf PSI zegt met een niet-openbaar Anthropic-model het Aaronson-Ambainis-vermoeden te hebben bewezen. Lean keurde het bewijs goed.
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.
OpenAI publiceert 722 wiskundepapers van intern model
OpenAI zet 722 wiskundige manuscripten van een nog niet uitgebracht model op GitHub. Een deel is met Lean gecontroleerd, de rest moet nog door wiskundigen worden beoordeeld.
AI helpt wiskundigen aan bewijs voor Euler-vergelijkingen
Anthropic-onderzoeker Levent Alpoge en NYU-wiskundige Tristan Buckmaster bewezen met hulp van Claude en Codex blow-up in eindige tijd voor de 3D Euler-vergelijkingen, machinaal gecontroleerd in Lean. Terence Tao noemt het een remarkable achievement.
Claude formaliseert Fermat in 13 miljoen regels Lean
Claude schreef in elf dagen een computergecontroleerd bewijs van Fermats laatste stelling: 13 miljoen regels Lean en 29.500 stellingen. Wat het wel en niet aantoont.
Lean checkt Astra’s wiskunde, peer review nog niet
OpenAI levert tien wiskundebewijzen van model Astra met machinecontrole in Lean 4. Verifieerbaar, maar nog niet door peer review.
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.