W lutym 2026 roku na Twitterze Bartosza Naskręckiego — prodziekana Wydziału Matematyki i Informatyki UAM w Poznaniu, badacza Centre for Credible AI w Warszawie — pojawił się wpis, który obiegł świat nauki: "Enrique emailed me a few weeks ago to casually chat about the elliptic curve DLP. We tested many of his ideas using models and Aristotle. I am very proud of him: in the breaks between high-school classes, he carved his way into the mathematical frontier, at the age of 17!"
Kim jest Enrique? Siedemnastoletni uczeń liceum, który w przerwach między lekcjami rozwiązał otwarty problem matematyczny z dziedziny kombinatoryki — problem powiązany z tradycją Paula Erdősa, jednego z najbardziej płodnych matematyków w historii.
Problem Erdősa: co to właściwie było
Paul Erdős (1913-1996) to legenda matematyki. Opublikował ponad 1500 prac naukowych, współpracował z ponad 500 matematykami. Słynął z formułowania problemów — otwartych pytań, które inspirowały całe pokolenia. Wiele z jego problemów pozostaje nierozwiązanych do dziś.
Problem, nad którym pracował Enrique, dotyczył krzywych eliptycznych i dyskretnego problemu logarytmicznego (DLP — Discrete Logarithm Problem). To jedno z fundamentalnych zagadnień kryptografii i teorii liczb. Rozwiązanie wymagało połączenia kombinatoryki, algebry i formalnego dowodzenia.
Rola AI: GPT Codex + Lean 4
Co wyróżnia tę historię od setek innych prac matematycznych? Enrique używał AI jako narzędzia pracy. Konkretnie: GPT Codex (model OpenAI specjalizowany w generowaniu kodu) do pisania formalnych dowodów w Lean 4 — asystencie dowodzenia matematycznego, który weryfikuje poprawność każdego kroku.
Sam Enrique potwierdził w odpowiedzi na pytanie Terence'a Tao: "I did use GPT Codex to write the Latex code and improve on some parts. I also had a lot of help from Bartosz Naskrecki."
To kluczowe: AI nie rozwiązało problemu ZA niego. AI pomogło mu: 1) Formalizować intuicję — przekładać pomysły na rygorystyczny język Lean 4 2) Pisać i poprawiać kod dowodowy — automatyzacja żmudnego "bookkeepingu" 3) Eksplorować warianty — szybkie testowanie różnych podejść 4) Weryfikować kroki — Lean potwierdza poprawność każdego fragmentu dowodu
Naskręcki był mentorem, który pomógł zweryfikować pomysły i nadać im kierunek. Ale sam przełom — kluczowa idea matematyczna — był dziełem 17-latka.
Terence Tao: "Nice work!"
Gdy rozwiązanie pojawiło się na Mathoverflow, skomentował je sam Terence Tao — medalista Fieldsa (2006), profesor UCLA, powszechnie uważany za najwybitniejszego żyjącego matematyka. Jego komentarz z 21 stycznia 2026: "Nice work! The way in which one handles the slow increase in k with n looks plausible to me, and it is good to have Lean confirm all the various bookkeeping and edge cases."
Tao zapytał wprost: "Were any AI tools used to create the informal proof?" — bo widział, że formalizacja w Lean była wyjątkowo czysta jak na licealistę. Odpowiedź była uczciwa: tak, użyto GPT Codex. Tao skomentował: "OK. Technically I guess this counts as AI-assisted."
Brak potępienia. Brak krytyki. Akceptacja. Najlepszy matematyk świata traktuje AI-assisted proofs jako normalną część pracy naukowej.
Dlaczego to jest przełomowe
Ta historia jest ważna z kilku powodów.
Po pierwsze — demokratyzacja nauki. 17-latek z liceum, z dostępem do internetu, AI i mentora, rozwiązał problem, nad którym mogliby pracować profesorowie z grant research. AI obniża barierę wejścia do poważnej matematyki. Nie potrzebujesz PhD, żeby wnieść wkład — potrzebujesz dobrego pomysłu i umiejętności pracy z narzędziami.
Po drugie — nowy model współpracy. Człowiek (intuicja, pomysł, kreatywność) + AI (formalizacja, weryfikacja, szybkość) + mentor (doświadczenie, kierunek). To nie jest "AI zamiast ludzi". To "ludzie z AI robią rzeczy, które wcześniej były niemożliwe".
Po trzecie — Polska na froncie. Bartosz Naskręcki z UAM nie jest przypadkową postacią — to badacz, którego problemy testują najnowsze modele AI na benchmarku FrontierMath od Epoch AI. GPT-5.4 rozwiązał jeden z jego problemów w testach. Polscy matematycy są na absolutnym froncie badań AI+nauka.
Lekcja dla wszystkich
Jeśli 17-latek z liceum, z pomocą AI, rozwiązuje otwarte problemy matematyczne — to co Ty możesz osiągnąć w SWOIM obszarze? Nie musisz być matematykiem. Musisz mieć problem do rozwiązania i umiejętność pracy z AI.
Naskręcki napisał na Twitterze: "Tego nie można pominąć! Siedemnastolatek uzbrojony w AI przy wsparciu Bartosza Naskręckiego z UAMu właśnie rozwiązał jeden z matematycznych problemów Erdosa!"
Ten wpis mówi wszystko. Nie "AI rozwiązało problem". Siedemnastolatek uzbrojony w AI. Narzędzie w rękach zdeterminowanego człowieka. To jest przyszłość — i ta przyszłość jest teraz.
Źródła: Bartosz Naskręcki (@nasqret) - wpis na Twitterze (luty 2026). Terence Tao - komentarz na Mathoverflow (21 styczeń 2026). Lean 4 - formalny asystent dowodzenia matematycznego. Epoch AI Research - FrontierMath benchmark. Paul Erdős - biogram i lista otwartych problemów. UAM Poznań - Wydział Matematyki i Informatyki.