--- title: "AI sformalizowała dowód wielkiego twierdzenia Fermata w 11 dni" description: "Agenci AI firmy Anthropic w 11 dni sformalizowali w języku Lean dowód wielkiego twierdzenia Fermata. Projekt objął 13 milionów linii kodu i około 29 500 twierdzeń pośrednich." publisher: "Najnowsze Informacje" language: "pl-PL" canonical_url: "https://najnowsze-informacje.pl/nauka/ai-sformalizowala-dowod-wielkiego-twierdzenia-fermata-w-11-dni" markdown_url: "https://najnowsze-informacje.pl/nauka/ai-sformalizowala-dowod-wielkiego-twierdzenia-fermata-w-11-dni/index.md" date_published: "2026-09-05T22:09:49.005Z" date_modified: "2026-09-05T22:29:13.417Z" author: "Redakcja" category: "Nauka" tags: - "sztuczna inteligencja" - "matematyka" - "wielkie twierdzenie fermata" - "formalizacja dowodów" - "lean" source_url: "https://www.newscientist.com/article/2587839-fermats-last-theorem-formalised-by-ai-agents-in-just-11-days/?utm_campaign=RSS|NSNS&utm_content=home&utm_medium=RSS&utm_source=NSNS" source_name: "New Scientist" image_url: "https://najnowsze-informacje.pl/api/media/file/nauka-unsplash-1788631289862.jpeg" image_alt: "a close up of a sheet of paper with numbers on it" image_credit: "© Bozhin Karaivanov / Unsplash" image_credit_url: "https://unsplash.com/@bkaraivanov" --- # AI sformalizowała dowód wielkiego twierdzenia Fermata w 11 dni > Agenci AI firmy Anthropic zapisali w języku Lean formalną wersję dowodu wielkiego twierdzenia Fermata, obejmującą 13 milionów linii kodu. ## Kluczowe informacje - Agenci AI pracowali nad formalizacją dowodu przez 11 dni. - Projekt obejmuje 13 milionów linii kodu w języku Lean. - Formalizacja dotyczy dowodu Andrew Wilesa i Richarda Taylora. - To wynik eksperymentu, a nie nowy dowód twierdzenia. Firma Anthropic poinformowała o stworzeniu formalnej wersji dowodu wielkiego twierdzenia Fermata. Według ogłoszenia projekt zajmował się zespół agentów AI pracujących z modelem Claude i został ukończony w ciągu 11 dni. Nie chodzi o znalezienie nowego dowodu, lecz o przepisanie znanego dowodu do postaci, którą komputer może sprawdzić krok po kroku. ## Twierdzenie, które czekało na dowód przez stulecia Wielkie twierdzenie Fermata mówi, że dla całkowitego n większego od 2 nie istnieją dodatnie liczby całkowite a, b i c spełniające równanie aⁿ + bⁿ = cⁿ. Samo twierdzenie jest łatwe do zapisania, ale znalezienie pełnego dowodu okazało się wyjątkowo trudne. Pierre de Fermat sformułował problem w XVII wieku i zasugerował, że zna rozwiązanie, lecz rzekomy dowód miał być zbyt długi, by zmieścić się na marginesie księgi. Przez kolejne stulecia matematycy próbowali bez powodzenia rozwiązać zagadkę. Andrew Wiles pracował nad nią przez siedem lat w tajemnicy. Przełom ogłosił w 1993 roku, a po wykryciu błędu w dowodzie wspólnie z Richardem Taylorem potrzebował około roku na jego usunięcie. Dowód został uznany za zakończony w 1995 roku. - Model Claude pracował z grupą agentów AI przez 11 dni, w sposób ciągły i autonomiczny. - Poszczególnym agentom przydzielano różne zadania, między innymi opracowanie mniejszych części twierdzenia. - Formalizacja obejmuje 13 milionów linii kodu w języku Lean oraz około 29 500 twierdzeń pośrednich. - Według Anthropic projekt jest ponad pięć razy większy od całej wcześniejszej pracy zgromadzonej w Mathlib i stanowi największy dotąd dowód zapisany w Lean. ## Po co formalizować dowody matematyczne Dowody matematyczne często składają się z wielu zależnych od siebie argumentów. Błąd w jednym kroku może podważyć całą konstrukcję, co pokazała historia dowodu Wilesa. Formalizacja matematyczna przenosi taki dowód z papieru do kodu. System sprawdzający może wtedy metodycznie kontrolować, czy każdy kolejny wniosek wynika z wcześniejszych założeń i reguł. Nie zastępuje to matematycznego znaczenia twierdzenia, ale ogranicza ryzyko przeoczenia błędu w długim łańcuchu rozumowania. W repozytorium Mathlib znajduje się już około 2 milionów linii sformalizowanej matematyki. ## Jak pracowali agenci AI Anthropic podało, że model Claude działał przez 11 dni bez przerwy, a nad projektem pracowało wiele odrębnych agentów AI. Każdy z nich otrzymywał inne zadania związane z fragmentami dowodu. Ludzie przekazywali im tylko ogólne instrukcje, które miały utrzymać pracę we właściwym kierunku. Nie wszystko przebiegało sprawnie. Kilka razy agenci tracili orientację w stanie projektu i przestawali skutecznie współpracować. Przełom nastąpił po wykorzystaniu narzędzia Prove2Me, stworzonego pierwotnie z myślą o współpracy matematyków. Pomagało ono agentom śledzić wykonane zadania i ustalać, czym należy zająć się dalej. ## Duży krok, ale nie koniec automatyzacji matematyki Rezultat Anthropic wyprzedził pięcioletni projekt Kevina Buzzarda z Imperial College London. Jego celem było formalizowanie około 100 stron dowodu Wilesa i Taylora w języku Lean, tak aby można było sprawdzić jego poprawność i wykorzystywać go jako podstawę dalszych badań. Buzzard oceniał wcześniej, że postępy AI mogą znacząco skrócić czas potrzebny na realizację tego zadania. Po ogłoszeniu Anthropic stwierdził, że formalizacja nie opiera się na dodatkowych założeniach poza aksjomatami matematyki. W projekcie pojawiły się między innymi elementy algebry, analizy harmonicznej, geometrii i teorii liczb. Bezpośrednim wynikiem jest więc sformalizowany i komputerowo sprawdzalny zapis istniejącego dowodu, a nie nowe rozwiązanie wielkiego twierdzenia Fermata. Szerszy wniosek, że AI będzie mogła automatycznie formalizować dużą część współczesnej literatury matematycznej, pozostaje perspektywą badawczą. Sam projekt pokazuje jednak, że automatyczna formalizacja może już obejmować bardzo długie, wielowarstwowe dowody, a przygotowany kod może stać się materiałem do dalszej pracy matematyków. ## Wyjaśnienie pojęć ### [Lean](https://najnowsze-informacje.pl/definicje/lean) Język programowania i system używany do zapisywania oraz formalnego sprawdzania dowodów matematycznych. ### [Mathlib](https://najnowsze-informacje.pl/definicje/mathlib) Wspólne repozytorium sformalizowanej matematyki wykorzystywane przez użytkowników języka Lean. ### [formalizacja matematyczna](https://najnowsze-informacje.pl/definicje/formalizacja-matematyczna) Przepisanie twierdzenia i jego dowodu do postaci kodu, który może być sprawdzany przez komputer krok po kroku. ### [autoformalizacja](https://najnowsze-informacje.pl/definicje/autoformalizacja) Automatyczne przekształcanie treści matematycznych, w tym dowodów, do postaci możliwej do sprawdzenia przez komputer. ## Źródło pierwotne [New Scientist](https://www.newscientist.com/article/2587839-fermats-last-theorem-formalised-by-ai-agents-in-just-11-days/?utm_campaign=RSS|NSNS&utm_content=home&utm_medium=RSS&utm_source=NSNS) --- ## Informacje do cytowania - **Autor:** Redakcja - **Data publikacji:** 2026-09-05T22:09:49.005Z - **Ostatnia aktualizacja:** 2026-09-05T22:29:13.417Z - **Kategoria:** Nauka - **Adres kanoniczny:** [https://najnowsze-informacje.pl/nauka/ai-sformalizowala-dowod-wielkiego-twierdzenia-fermata-w-11-dni](https://najnowsze-informacje.pl/nauka/ai-sformalizowala-dowod-wielkiego-twierdzenia-fermata-w-11-dni) - **Wersja Markdown:** [https://najnowsze-informacje.pl/nauka/ai-sformalizowala-dowod-wielkiego-twierdzenia-fermata-w-11-dni/index.md](https://najnowsze-informacje.pl/nauka/ai-sformalizowala-dowod-wielkiego-twierdzenia-fermata-w-11-dni/index.md) **Sugerowane cytowanie:** > Najnowsze Informacje, „AI sformalizowała dowód wielkiego twierdzenia Fermata w 11 dni”, 2026-09-05, https://najnowsze-informacje.pl/nauka/ai-sformalizowala-dowod-wielkiego-twierdzenia-fermata-w-11-dni