Fermatova věta: rébus, který odolával 350 let
Pro pořádek rychlé opáčko. Fermatova poslední věta tvrdí, že rovnice aⁿ + bⁿ = cⁿ nemá žádné celočíselné řešení, když je exponent n větší než 2. Pro n = 2 je to známá Pythagorova věta s nekonečně mnoha řešeními (3, 4, 5). Ale jakmile exponent zvednete na trojku, čtverku a výš, všechna celočíselná řešení zmizí.
Pierre de Fermat si tohle tvrzení načmáral roku 1637 na okraj knihy s poznámkou, že má „skutečně úžasný důkaz", ale že se mu nevejde na okraj. Žádný důkaz se nikdy nenašel. Trvalo přes 350 let, než větu v roce 1994 dokázal britský matematik Andrew Wiles — mimochodem bez použití počítače. Za důkaz dostal Abelovu cenu, jakousi Nobelovku pro matematiky, a v roce 1999 ho královna Alžběta II. povýšila do šlechtického stavu.
Co přesně Claude udělal — a co neudělal
Tady je ta klíčová pointa, kterou většina titulků zazdí. Claude Fermatovu větu nevyřešil. To udělal Wiles před třiceti lety. Claude vzal ten už přijatý lidský důkaz a přepsal ho do jazyka, který dokáže zkontrolovat počítač — a to celé stihl za 11 dní.
Podle oznámení Anthropicu na tom pracovaly desítky agentů Claude, kteří argument převedli do 13 milionů řádků jazyka Lean. Po cestě dokázali víc než 30 000 pomocných vět, z nichž 29 500 nakonec použili ve finální konstrukci.
Pro srovnání: lidský tým vedený Kevinem Buzzardem z Imperial College London běží s formalizací Fermatovy věty od roku 2024 a počítal s tím, že mu to zabere zhruba pět let. Claude tu úlohu sfoukl za necelé dva týdny. Buzzard před spuštěním Claude říkal, že je si správností důkazu „jistý na 99,9 %". Po něm: „Teď na 100 %."
Lean: kontrola pravopisu pro matematiku
Co to vlastně znamená „formalizovat důkaz"? Matematikové píšou důkazy pro lidi — přeskočí kroky, které jim připadají samozřejmé, a odkazují na výsledky dokázané jinde. Jenže občas se do toho vloudí chyba, na kterou se přijde až po letech.
Formalizace znamená rozepsat každý jednotlivý krok tak, aby si ho mohl zkontrolovat stroj. Je to trochu jako přepsat recept pro zkušeného kuchaře do podoby pro robota, který neuzná nic, co není odvozené krok po kroku. „Přidej sůl podle chuti" se musí rozepsat na „přidej 3,2 gramu soli". Každá definice, každý předpoklad, každá logická návaznost. A právě proto se Wilesův důkaz nafoukne do 13 milionů řádků.
Software, který tohle kontroluje, se jmenuje Lean a je volně dostupný. Projde důkaz řádek po řádku a odmítne ho, jakmile nějaký krok nevyplývá z předchozího. Žádné „tady si jsem tím jistý".
Účet: 6 miliard tokenů
A teď něco pro ty, co mají rádi konkrétní čísla. Celý běh Claude spolykal zhruba 6 miliard výstupních tokenů. Podle publikovaných komerčních cen Anthropicu by to vyšlo na asi 300 tisíc dolarů, tedy v přepočtu přes šest milionů korun. Když si to rozpočítáte, vychází to zhruba na 50 dolarů za milion výstupních tokenů. Interní náklady Anthropicu budou nejspíš výrazně nižší — ale i tak je to krásná ukázka, proč formalizace doposud nebyla masová záležitost.
Dobrá zpráva je, že cena výpočetního výkonu padá. Co dnes stojí statisíce, bude za pár let dostupné univerzitním týmům i v Evropě.
Háček: správný důkaz ještě není použitelný důkaz
A tady se dostáváme k té méně sexy části příběhu. Buzzard upozornil na takzvaný „scénář noční můry": Claude svůj výstup nepostavil jako čistou, znovupoužitelnou knihovnu. Těch 13 milionů řádků je víc než pětinásobek velikosti Mathlib, sdílené knihovny, na kterou matematici spoléhají.
Kdyby budoucí AI systémy chrlily tisíce správných důkazů, z nichž každý by si s sebou táhl vlastní nepřehlednou hromadu podpůrné matematiky, počítače by sice jednotlivé výsledky ověřily, ale matematici by na nich nedokázali efektivně stavět. Jak trefně napsal Buzzard na svém blogu: „matematicky nám tahle práce Anthropicu říká v podstatě nic" — protože samotný důkaz už matematici dávno přijali.
Skutečná hodnota je jinde. Formalizace dává matematice něco, co nikdy neměla: automatického druhého čtenáře, který se neunaví a dokáže přesně ukázat, kde argument selže. To může být zásadní v době, kdy jsou matematické články čím dál delší a recenzní řízení podle matematiků nestíhá.
A vedle toho: drama kolem Navier–Stokese
Zatímco Claude „jen" ověřoval starý důkaz, OpenAI mezitím oznámila něco ambicióznějšího. Tvrdí, že našla řešení problému Navier–Stokes, jednoho ze sedmi problémů tisíciletí, za které Clayův institut vyplácí milion dolarů. Podle The Verge na tom pracovalo 10 000 souběžných agentů.
Jenže ani tady to není bez kontroverze. Den před oznámením OpenAI publikovali svůj vlastní postup matematik Tristan Buckmaster z NYU a výzkumník Anthropicu Levent Alpöge. Buckmaster se ptal, jestli OpenAI nevyužila data z jejich pracovních sezení v Codex, kam ukládali koncepty celého projektu. OpenAI to popírá a zároveň oznámila, že milionovou odměnu si nárokovat neplánuje. Porota, jak píše Mind Matters, zatím zvažuje důkazy.
Co z toho plyne
Pokud si z toho máte odnést jednu věc, tak tuhle: schopnost ověřovat důkazy je možná důležitější než schopnost je vymýšlet. Číselný teoretik Alex Kontorovich z Rutgers řekl, že ho výsledek „naprosto odzbrojil". Daniel Litt z univerzity v Torontu zase: „Když zformalizují Fermatovu větu, zvládnou nejspíš cokoliv."
Pro běžného uživatele Claude to nic nemění — tohle není funkce, kterou si zapnete v chatu v češtině. Je to ale důkaz, že jazykové modely dokážou dělat úplně jinou práci, než je psaní e-mailů a shrnování textu. A že hranice mezi „psát" a „ověřovat" je teď překvapivě tenká.
Řeší Claude skutečně nové matematické problémy, nebo jen ověřuje staré důkazy?
U Fermatovy věty šlo čistě o formalizaci — Claude převedl už existující a ověřený důkaz Andrewa Wilese do strojově kontrolovatelné podoby. Novou matematiku neobjevil. Rozdíl je podstatný: ověřování je dřina, ale vynález nového tvrzení je něco úplně jiného. Právě proto se samostatné „objevy" (například tvrzení OpenAI u Navier–Stokese) posuzují mnohem přísněji.
Můžu si formalizaci důkazu zkusit sám s běžným Claude?
Ne tak, jak to udělal Anthropic. Šlo o výzkumný běh s desítkami koordinovaných agentů na specializované platformě Prove2Me, ne o běžnou konverzaci v chatu. Jazyk Lean si ale můžete stáhnout zdarma a zkoušet s ním menší důkazy i ručně nebo s asistencí modelu.
Kolik stálo formalizování Fermatovy věty?
Běh spotřeboval zhruba 6 miliard výstupních tokenů, což by podle publikovaných komerčních cen Anthropicu vyšlo na přibližně 300 tisíc dolarů (přes šest milionů korun). Interní náklady firmy byly zřejmě nižší a s klesající cenou výpočetního výkonu se podobné projekty stávají dostupnějšími.
