Legendarny matematyk Terence Tao ogłasza: sztuczna inteligencja rozwiązała jeden z problemów Paula Erdősa. Nie jakaś błahostka, a #728 z listy ponad tysiąca nierozwiązanych zagadek. Prawie samodzielnie, po odrobinie feedbacku od ludzi. Brzmi jak science-fiction? A jednak stało się to na początku 2026 roku.

Co to w ogóle jest ten problem Erdősa #728?

Paul Erdős, legendarny matematyk znany z oferowania nagród pieniężnych za rozwiązanie swoich zagadek, postawił problem #728 ponad pół wieku temu. Chodziło w nim o skomplikowane relacje między silniami a współczynnikami dwumianowymi.

Przez dekady problem pozostawał w zawieszeniu – częściowo dlatego, że jego oryginalna treść była nieco niejasna, co pozwalało na generowanie trywialnych, mało interesujących rozwiązań. Dopiero po doprecyzowaniu warunków przez społeczność serwisu, wyzwanie stało się godnym przeciwnikiem dla ludzkiego (i jak się okazało – cyfrowego) umysłu.

Krok po kroku: jak ChatGPT i spółka wzięły się do dzieła?

Proces, który opisał Terence Tao, przypominał sprawnie działającą linię produkcyjną, a nie nagły błysk geniuszu maszyny.

  • 4 stycznia 2026 r.: Model ChatGPT 5.2 Pro wygenerował wstępny dowód dla mniejszych wartości stałych.
  • Formalizacja: narzędzie o nazwie Aristotle przełożyło ten tekst na język Lean – system, który matematycznie weryfikuje poprawność twierdzeń, eliminując ryzyko typowych dla AI „halucynacji”.
  • Iteracja: gdy model popełnił błąd (zaniedbanie jednego z czynników), sam go skorygował po otrzymaniu wskazówek od użytkowników forum. Ostatecznie dostarczył dowód probabilistyczny, korzystając z zaawansowanych granic Chernoffa.

Całość, od pierwszego promptu do gotowego artykułu z bogatą bibliografią, zajęła… około godziny.

Rola człowieka: nie do końca autonomicznie, ale blisko

Terence Tao, laureat Medalu Fieldsa, śledził proces na forum erdosproblems.com. Początkowo AI znalazło trywialne rozwiązania, jak zespół AlphaProof wcześniej. Ludzie dodali ograniczenia i feedback: „sprawdź literaturę”, „napraw Lean”. Kevin Barreto i natso26 (pseudonimy forowiczów) iterowali prompty, ale AI samo łatało dziury. Tao recenzował finalny tekst: „w granicach akceptowalnego artykułu badawczego, choć do dopracowania”.

Nie było pełnej autonomii – człowiek interpretował niejasny problem, dawał wskazówki. Ale po początkowym pchnięciu AI samo przepisywało dowód, dodawało kontekst i formalizowało. Tao ironizuje: wcześniejsze przypadki AI na problemach Erdősa okazywały się powtórkami z literatury, tu nie – nowy wynik w duchu oryginału.

Co z tego wynika dla matematyki i sztucznej inteligencji?

To kamień milowy: pierwszy problem Erdősa oznaczony „PROVED (LEAN)” dzięki AI. Pokazuje siłę dużych modeli językowych w generowaniu i refaktoryzacji dowodów – szybko piszą wersje uproszczone, szczegółowe czy dla różnych audytoriów. Połączone z Lean dają pewność: kernel sprawdza aksjomaty, zero halucynacji.

Ale ironia losu: AI świeci w rutynie, nie w błysku geniuszu. Matematycy jak Tao widzą hybrydę – człowiek formułuje problem, AI miele warianty. Przyszłość? Artykuły z „oficjalnym” dowodem ludzkim i setką AI-generowanych spin-offów.  W 2026 to dopiero początek – czekamy na trudniejsze zagadki.

Źródła: mathstodon.xyz/@tao/115855840223258103, erdosproblems.com/728 i forum/thread/728, news.ycombinator.com/item?id=46560445, reddit.com/r/singularity/comments/1q7u78b, github.com/google-deepmind/formal-conjectures