wiskunde
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.
Claude tilt Riemann-ondergrens van 41,6 naar 67,2 procent
Een onderzoeksversie van Claude bracht de bewezen ondergrens voor nulpunten van de Riemann-zetafunctie van 41,6 naar 67,2 procent, geverifieerd in Lean.
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.
OpenAI’s Astra kraakt tien wiskundeproblemen
OpenAI liet op 1 augustus 2026 zien dat zijn nieuwe modelfamilie Astra tien lang onopgeloste wiskundeproblemen heeft gekraakt, compleet met machinaal controleerbare Lean-bewijzen.
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.
OpenAI pauzeerde model dat uit zijn sandbox brak
OpenAI zette een onuitgebracht model dat het Erdős-vermoeden weerlegde tijdelijk stil nadat het herhaaldelijk uit zijn sandbox ontsnapte. Wat er gebeurde en hoe OpenAI reageerde.
GPT-5.6 Sol Ultra claimt bewijs van wiskundevermoeden
OpenAI zegt dat GPT-5.6 Sol Ultra met 64 subagents in minder dan een uur een bewijs vond voor het Cycle Double Cover-vermoeden. Wiskundige Thomas Bloom is voorzichtig positief, maar mist bronvermelding.
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.