Thema: Lean
OpenAI löst 377 Mathematikprobleme – doch ein Beweis steht infrage
Artikel
OpenAI veröffentlichte KI-generierte Beweise für 377 offene Mathematikfragen, darunter die Unique Games Conjecture. Doch ein möglicher Fehler im Navier-Stokes-Beweis in Lean wirft Fragen zur Verifizierbarkeit auf.
DeepMind-KI beweist neun Erdős-Probleme
Artikel
AlphaProof Nexus von Google DeepMind hat neun bislang ungelöste Erdős-Probleme gelöst und 44 OEIS-Vermutungen formal bewiesen. Lean prüft jeden Schritt maschinell – doch der Großteil der Aufgaben bleibt offen.
