Lean

AI od DeepMind vyřešila devět Erdősových problémů

Google DeepMind, součást společnosti Alphabet, publikoval recenzovanou zprávu o AlphaProof Nexus, systému umělé inteligence, který vyřešil devět otevřených problémů matematika Paula Erdőse a dokázal 44 domněnek z On-Line encyklopedie celočíselných posloupností (OEIS). Článek vyšel ve čtvrtek 8. října v časopise…

OpenAI stahuje tři matematické studie kvůli chybě ve znaménku

Společnost OpenAI stáhla tři ze 722 matematických rukopisů, které zveřejnila 6. října, a to necelý den po jejich publikaci. Firma objevila chybu ve znaménku, která znehodnotila argumentaci v jedné studii a konstrukci, na které závisely dvě další práce. Zároveň revidovala…

Výzkumníci upozorňují na nesrovnalosti v důkazu Navierových-Stokesových rovnic od OpenAI

Matematici prověřují velkou sadu důkazů vytvořených umělou inteligencí, které společnost OpenAI zveřejnila 6. října, a některé dosavadní nálezy vyvolávají pochybnosti. Tým vedený výzkumníky z Cambridge tvrdí, že verze dřívějšího důkazu Navierových-Stokesových rovnic, která je čitelná pro člověka, a verze ověřitelná…

OpenAI zveřejnila 722 matematických prací od dosud nevydaného AI modelu

V úterý 6. října zveřejnila společnost OpenAI 722 matematických rukopisů ve veřejném úložišti na GitHubu, roztříděných do 372 "rodin výsledků". Společnost tvrdí, že je vytvořil dosud nevydaný interní model. Časopis Scientific American uvedl, že úložiště bylo spuštěno v 18:00 východoamerického…

Anthropic: AI model Claude dokázal Velkou Fermatovu větu

Společnost Anthropic ve čtvrtek oznámila, že její model umělé inteligence Claude dokončil první počítačem ověřený důkaz Velké Fermatovy věty, jednoho z nejslavnějších výsledků v matematice. Claude pracoval převážně autonomně po dobu 11 dní a napsal důkaz v programovacím jazyce Lean,…