{"data":{"id":2390,"lang":"cs","title":"Anthropic: Claude za 11 dní formalizoval kompletní důkaz Velké Fermatovy věty","summary":"Claude samostatně vytvořil 13milionový řádkový, počítačem ověřený formální důkaz Velké Fermatovy věty v Lean za pouhých 11 dní.","category":"ai","category_label":"AI","published_at":"2026-09-05T10:01:22Z","updated_at":"2026-09-05T10:01:22Z","url":"https://techtools.cz/tools/news/clanek/2390-anthropic-claude-za-11-dni-formalizoval-kompletni-dukaz-velke-fermatovy-vety","api_url":"https://techtools.cz/news-api/v1/articles/2390?lang=cs","markdown_url":"https://techtools.cz/news-api/v1/articles/2390.md?lang=cs","image_url":"https://www-cdn.anthropic.com/images/4zrzovbb/website/578f91575c42231f0994e341014614255149af80-1200x630.jpg","word_count":189,"reading_time_minutes":1,"sources":[{"url":"https://www.anthropic.com/research/formalizing-fermats-last-theorem","domain":"anthropic.com"},{"url":"https://siliconangle.com/2026/09/04/anthropic-uses-claude-to-formalize-proof-of-fermats-last-theorem/","domain":"siliconangle.com"}],"translation":{"lang":"en","id":2317,"title":"Anthropic Says Claude Formalized a Full Proof of Fermat's Last Theorem in 11 Days","url":"https://techtools.cz/tools/news/article/2317-anthropic-says-claude-formalized-a-full-proof-of-fermat-s-last-theorem-in-11","api_url":"https://techtools.cz/news-api/v1/articles/2317?lang=en"},"content":"Anthropic oznámil, že jeho modely Claude vytvořily první úplný, počítačem ověřený důkaz Velké Fermatovy věty v jazyce Lean, a to během 11 dnů v srpnu 2026 z velké části samostatně. Běh vygeneroval 13 milionů řádků kódu v Lean a dokázal 30 300 vět, z nichž 29 500 bylo použito ve finálním důkazu, přičemž spotřeboval zhruba šest miliard výstupních tokenů.\n\nDůkaz formalizuje zjednodušenou verzi přelomového argumentu Andrewa Wilese z roku 1995 podle výkladu matematiků Henriho Darmona, Freda Diamonda a Richarda Taylora. Matematici dříve odhadovali, že formalizace Wilesova důkazu zabere lidem několik let práce; podle Anthropicu to jeho interní výzkumný model zvládl za necelé dva týdny. Výsledek je zhruba pětkrát větší než Mathlib, hlavní komunitně spravovaná knihovna formalizované matematiky, a Lean jej ověřil pouze pomocí svých tří standardních axiomů.\n\nPráce vznikla na platformě Prove2Me, otevřené kolaborativní platformě navržené Tianyi Pengem a jeho spolupracovníky na Columbijské univerzitě, která udržuje orientovaný acyklický graf matematických vět a koordinuje více AI agentů pracujících na něm současně. Anthropic tento úspěch prezentuje jako důkaz, že AI dokáže formalizovat složité matematické důkazy ve velkém měřítku, což by mohlo ulehčit ověřování matematikům a umožnit rychlejší recenzní řízení budoucích výsledků."}}