Společnost OpenAI zpřístupnila na platformě GitHub stovky matematických studií a důkazů formálně zapsaných v jazyce Lean, které mají řešit desítky otevřených vědeckých problémů.
Společnost OpenAI nahrála 6. října na web stovky nových matematických důkazů řešících dosud otevřené problémy[1]. Na vývojářské platformě GitHub naráz zpřístupnila 722 matematických studií, které mají řešit zhruba 372 dosud otevřených matematických problémů[2]. K tomuto bezprecedentnímu kroku přistoupila OpenAI na základě doporučení své poradní skupiny, v níž zasedají přední matematici Timothy Gowers a Edward Witten[3]. Rozsah tohoto průlomu vynikne při srovnání s nedávnou minulostí: ještě na začátku roku 2023 získal ChatGPT ve středoškolské matematické soutěži pouze 30 bodů ze 150[4].
Výkon interního modelu a role jazyka Lean
Zveřejněným objevům předcházelo testování interních systémů na rozsáhlé sadě úloh. Interní model OpenAI dostal k dispozici databázi čtyř tisíc otevřených matematických problémů a více než tři sta z nich dokázal zapsat ve formálním jazyce Lean[5]. Pro některé z těchto 372 přelomových výsledků OpenAI existuje formální certifikát v jazyce Lean[6].
Celý proces byl náročný také po výpočetní stránce. Výpočetní výkon na vyřešení jednoho problému odpovídal podle vyjádření OpenAI zhruba třem hodinám běhu ChatGPT Pro[7]. Ani automatizované dokazování se však nevyhnulo nedostatkům. Společnost OpenAI následně stáhla tři z publikovaných textů kvůli nalezeným chybám[8].
Průlomy v teoretické informatice a předchozí pokusy
Mezi publikovanými pracemi se nachází řešení řady otázek, se kterými si odborníci dlouho nevěděli rady. Mezi zveřejněnými pracemi byl algoritmus Fourierovy transformace a násobení celých čísel v čase O(n log0.9999999999999 n)[9].
Říjnové publikaci předcházely další kroky OpenAI na poli exaktních věd. Již v září OpenAI zveřejnila údajné řešení Navier-Stokesových rovnic, na které nasadila desítky tisíc AI agentů[10]. Právě při oznámení řešení Navier-Stokesových rovnic doprovodila OpenAI neformální důkaz formální reprezentací v jazyce Lean[11].
Formální verifikace a reakce komunity
Závody ve formálním ověřování neprobíhají pouze v laboratořích OpenAI. Společnost Anthropic oznámila, že model Claude formálně ověřil Velkou Fermatovu větu pomocí 13 milionů řádků kódu napsaných během 11 dnů[12].
Tento rozvoj úzce souvisí se vzestupem komunitních nástrojů pro formální zápis matematických teorií. Otevřená knihovna Mathlib pro formální matematiku byla oceněna cenou Jean-Pierre Demailly Prize pro rok 2026 a podílí se na ní 65 recenzentů a 950 přispěvatelů[13]. Standardy ověřování navíc přímo ovlivňují vědecké publikování: podmínkou přijetí práce bude formální ověření důkazů v systému Lean[14].
Masivní nástup umělé inteligence však vyvolává i odpor části akademické sféry. Skupina nazvaná Association for Human Mathematics vydala prohlášení odsuzující vydání výsledků společností OpenAI[15]. Rychlost, s jakou modely řeší otevřené problémy, tak otevírá zásadní otázky o budoucí roli lidských matematiků.
Pro některé z 372 přelomových výsledků OpenAI existuje formální certifikát v jazyce Lean.
There’s a Lean certificate, as there are for some of the other 372 breakthrough results (not all of them).
scottaaronson.blogOtevřít zdroj
Společnost OpenAI následně stáhla tři z publikovaných textů kvůli nalezeným chybám.
Říjnový „balík důkazů“ nebyl dokonalý. Tři texty už firma kvůli objeveným chybám vzápětí stáhla.
seznamzpravy.czOtevřít zdroj
Mezi zveřejněnými pracemi byl důkaz rovnosti L=BPL a algoritmus Fourierovy transformace a násobení celých čísel v čase O(n log0.9999999999999 n).
- The Fourier Transform and integer multiplication in less than O(n log n) time, breaking a barrier that had stood since the 1960s. The new running time, if you’re curious, is O(n log0.9999999999999 n), give or take some 9’s.
scottaaronson.blogOtevřít zdroj
V nově plánovaném matematickém časopise bude podmínkou přijetí práce formální ověření důkazů v systému Lean.
To be accepted, a paper will need to have its proofs formally verified in Lean.
terrytao.wordpress.comOtevřít zdroj
OpenAI zveřejnila 372 matematických výsledků na základě doporučení své poradní skupiny, v níž zasedají Timothy Gowers a Edward Witten.
And yes, among the 372 huge results released yesterday by OpenAI, on the recommendation of its advisory group of Timothy Gowers, Edward Witten, and other distinguished mathematicians, was a proof of Subhash Khot’s Unique Games Conjecture (UGC)
scottaaronson.blogOtevřít zdroj
OpenAI zveřejnila na repozitáři GitHub 722 matematických studií, které mají řešit zhruba 372 dosud otevřených matematických problémů.
V říjnu totiž OpenAI udělala něco dosud nevídaného. Naráz na repozitáři Github zveřejnila 722 matematických studií, které mají řešit asi 372 dosud otevřených matematických problémů.
seznamzpravy.czOtevřít zdroj
Společnost OpenAI nahrála 6. října na web stovky nových matematických důkazů řešících dosud otevřené problémy.
Stovky nových matematických důkazů nahrála firma OpenAI na web 6. října. Mnohé z nich nabízejí řešení tzv. „otevřených problémů“, tedy otázek, na které matematika zatím neznala odpovědi.
seznamzpravy.czOtevřít zdroj
Skupina nazvaná Association for Human Mathematics vydala prohlášení odsuzující vydání výsledků společností OpenAI.
Meanwhile, something calling itself the Association for Human Mathematics put out a statement condemning OpenAI for its release. The statement included a sentence that’s since been widely mocked on social media: “Mathematicians did not ask for this work to be done.”
scottaaronson.blogOtevřít zdroj
Výpočetní výkon na vyřešení jednoho problému odpovídal podle vyjádření OpenAI zhruba třem hodinám běhu ChatGPT Pro.
Podle vyjádření OpenAI to zvládl jejich interní model na jeden pokus: „Na vyřešení jednoho problému byl vynaložen výpočetní výkon, který odpovídá asi třem hodinám běhu ChatGPT Pro.“
seznamzpravy.czOtevřít zdroj
Otevřená knihovna Mathlib pro formální matematiku byla oceněna cenou Jean-Pierre Demailly Prize pro rok 2026 a podílí se na ní 65 recenzentů a 950 přispěvatelů.
Mathlib is an open-source community-driven library that supports the formal mathematical ecosystem and was awarded the 2026 Jean-Pierre Demailly Prize for Open Science in Mathematics. It is curated by a team of 65 reviewers and 950 contributors to date.
xenaproject.wordpress.comOtevřít zdroj
Společnost Anthropic oznámila, že model Claude formálně ověřil Velkou Fermatovu větu pomocí 13 milionů řádků kódu napsaných během 11 dnů.
When Anthropic announced that Claude had formally verified Fermat’s Last Theorem with 13 million lines of code written over 11 days, Kevin Buzzard cheerfully lauded the result while also declaring he had no intention of ending his ongoing formalization of a more modern proof.
xenaproject.wordpress.comOtevřít zdroj
Při oznámení řešení Navier-Stokesových rovnic doprovodila OpenAI neformální důkaz formální reprezentací v jazyce Lean.
When OpenAI announced solutions to the Navier–Stokes equations that blow up in finite time, the natural-language proof was accompanied by a Lean formalization.
xenaproject.wordpress.comOtevřít zdroj
Interní model OpenAI dostal databázi čtyř tisíc otevřených matematických problémů a více než tři sta z nich zapsal ve formálním jazyce Lean.
Výzkumníci dali internímu (dosud neveřejnému) AI modelu databázi čtyři tisíc nevyřešených matematických problémů, a model více než tři stovky z nich dokázal zapsat v jazyce Lean, což víceméně zaručuje, že důkaz je jednoznačně ověřený a platný.
seznamzpravy.czOtevřít zdroj
Na začátku roku 2023 získal ChatGPT ve středoškolské matematické soutěži pouze 30 bodů ze 150.
Ještě na začátku roku 2023 měl ChatGPT problém i s jednoduchými matematickými operacemi a ve středoškolské matematické soutěži dostal jen 30 bodů ze 150.
seznamzpravy.czOtevřít zdroj
V září OpenAI zveřejnila údajné řešení Navier-Stokesových rovnic, na které nasadila desítky tisíc AI agentů.
Už v září firma OpenAI v matematické komunitě vzbudila rozruch, když publikovala údajné řešení Navier-Stokesových rovnic, jednoho ze šesti nevyřešených „problémů tisíciletí“. Na řešení výzkumníci nasadili desítky tisíc AI agentů, kteří vyprodukovali formální důkaz a 166stránkové „vysvětlení“.
seznamzpravy.czOtevřít zdroj