Wykład „Impossibility results in dynamical systems” dotyczył pytania, które w matematyce pojawia się bardzo często: czy dla danej klasy obiektów można znaleźć prosty sposób rozstrzygania, kiedy dwa z nich są w istocie takie same? W klasycznych przypadkach rolę takiego kryterium pełni na przykład rodzaj powierzchni, postać Jordana macierzy czy entropia układu.

W przypadku bardziej złożonych układów dynamicznych sytuacja może wyglądać zupełnie inaczej. Jednym z głównych tematów wykładu były wyniki pokazujące, że niektórych takich obiektów nie da się sklasyfikować za pomocą konkretnego niezmiennika czy innego prostego kryterium. Warto przy tym zauważyć, że w nagrodzonym wyniku wykorzystano twierdzenie o selektorach Czesława Rylla-Nardzewskiego. W drugiej części wykładu pojawił się również problem Rufusa Bowena dotyczący klasyfikacji układów symbolicznych posiadających własność specyfikacji – silną własność pozwalającą łączyć odpowiednio odległe fragmenty dynamiki. Okazuje się, że nawet w tej dobrze określonej klasie klasyfikacja za pomocą konkretnego niezmiennika pozostaje niemożliwa.

To właśnie ten rodzaj wyników dobrze pokazuje jedną z charakterystycznych cech współczesnej matematyki: czasem ważnym rezultatem nie jest znalezienie rozwiązania problemu, lecz precyzyjne wykazanie, że określony sposób jego rozwiązania jest niemożliwy.

„Mathematical discovery in the age of AI” Bartosza Naskręckiego był poświęcony pytaniu, jak sztuczna inteligencja zmienia sposób, w jaki matematycy poszukują nowych wyników, formułują hipotezy i konstruują dowody.

Wykład rozpoczął się od przykładów pokazujących możliwości współczesnych modeli AI w rozwiązywaniu problemów matematycznych. Jednym z omawianych przykładów był FrontierMath – projekt przygotowujący problemy na poziomie wymagającym zaawansowanych kompetencji matematycznych, których rozwiązania mają być jednoznaczne i możliwe do komputerowej weryfikacji.

Ważną częścią wykładu była formalizacja matematyki, czyli zapisywanie definicji, twierdzeń i dowodów w języku zrozumiałym dla komputera. Naskręcki pokazał na przykładzie systemu Lean, jak formalny dowód może zostać zweryfikowany przez maszynę, a także jak rozwijana społecznościowo biblioteka mathlib pozwala gromadzić formalnie sprawdzone wyniki matematyczne.

Kolejny krok stanowi połączenie formalizacji z AI. Modele językowe mogą nie tylko generować odpowiedzi, ale również eksplorować możliwe strategie dowodzenia, proponować kolejne kroki i współpracować z systemami formalnej weryfikacji. Wśród przykładów omawianych podczas wykładu znalazły się m.in. LeanDojo, AlphaProof, AlphaGeometry, FunSearch i AlphaEvolve.

AI może być więc czymś więcej niż narzędziem służącym do sprawdzania lub przyspieszania pracy matematyka – może uczestniczyć również w samym procesie poszukiwania rozwiązania. Przykładem są przedstawione podczas wykładu próby automatyzacji kolejnych etapów pracy – od formalizacji i analizy rozwiązania, przez jego weryfikację, aż po dalsze poszukiwania.

Wykład prowadził więc do szerszego pytania: gdzie przebiega granica między narzędziem wspomagającym matematyka a systemem, który rzeczywiście uczestniczy w matematycznym odkryciu? Pytanie to nabiera szczególnego znaczenia w sytuacji, gdy AI może nie tylko proponować rozwiązania, ale także współpracować z systemami formalnej weryfikacji, które pozwalają komputerowo sprawdzić poprawność dowodu.

Akcja opery rozpoczyna się podczas IV Ogólnopolskiego Kongresu Genetycznego we Wrocławiu. Jej główny bohater, genetyk prof. Teodor Zaks, przedstawia podczas konferencji teorię dotyczącą możliwości rozpoznawania, przewidywania, a nawet kształtowania wyjątkowych ludzkich zdolności poprzez odpowiednią konfigurację genów. Poszukiwanie „genu doskonałości” prowadzi go jednak do konfrontacji z pytaniami o granice nauki, ludzkiej ambicji oraz cenę dążenia do ideału.

To właśnie tutaj świat opery spotkał się ze światem współczesnej nauki. „GenOM” stawia pytania o granice naukowego poznania, ludzkiej ambicji i dążenia do doskonałości. Czy wszystko, co można zmierzyć i przewidzieć, powinno być również poddane optymalizacji? Czy możliwość technicznego rozwiązania problemu oznacza, że powinniśmy to rozwiązanie zastosować? I wreszcie – czy doskonałość, którą można zaprojektować, rzeczywiście jest tym samym, czego jako ludzie pragniemy?

Pytania te nie pozostają jednak wyłącznie domeną świata przedstawionego w operze. Współczesna nauka coraz częściej dysponuje narzędziami, które pozwalają nie tylko opisywać i przewidywać złożone zjawiska, ale także coraz skuteczniej poszukiwać ich optymalnych rozwiązań. Dotyczy to również matematyki, w której sztuczna inteligencja zaczyna odgrywać coraz większą rolę w procesie rozwiązywania problemów i odkrywania nowych zależności.

W tym sensie spotkanie matematyków z „GenOM-em” tworzyło szczególnie ciekawy dialog. W operze naukowiec próbuje odnaleźć i zaprogramować biologiczną doskonałość. Współczesna matematyka staje natomiast przed pytaniem, co stanie się z ludzkim sposobem odkrywania, gdy coraz bardziej zaawansowane modele AI zaczną uczestniczyć w tworzeniu matematycznej wiedzy. W obu przypadkach powraca więc pytanie nie tylko o granice optymalizacji, lecz także o granice ludzkiego autorstwa: kto pozostaje autorem odkrycia, gdy człowiek wyznacza cel, ale droga do jego osiągnięcia zostaje odnaleziona przez system AI?

Co ciekawe, „GenOM” wyrasta z rzeczywistego spotkania nauki i sztuki – inspiracją dla libretta był wykład genetyka prof. Michała Witta „Geny a muzyka”. Wieczór w Operze stał się więc czymś więcej niż tylko wydarzeniem towarzyszącym konferencji. Był kolejnym sposobem rozmowy o nauce – tym razem za pomocą muzyki, teatru i współczesnego języka operowego.