Wyobraź sobie pokój wypełniony najlepszymi umysłami świata, w którym zamiast szelestu kartek słychać jedynie stukanie w klawiatury. Podczas gdy turyści w Londynie szukają cienia w trakcie fali upałów, grupa 25 naukowców zamknięta w sali bez okien mierzy się z wyzwaniem, które przez wieki było symbolem matematycznej niemożliwości.
Jeszcze do niedawna wydawało się, że dowodzenie twierdzeń to ekskluzywna domena ludzkiego intelektu. Dziś, dzięki nowym modelom AI, tempo pracy wystrzeliło w górę, a matematycy zaczynają zadawać sobie pytanie: czy wkrótce staniemy się tylko obserwatorami własnej nauki?
Cyfrowy fundament matematyki
Wielkie Twierdzenie Fermata, sformułowane w XVII wieku, wydaje się proste: równanie aⁿ + bⁿ = cⁿ nie ma rozwiązań w liczbach całkowitych, jeśli n jest większe od 2. Mimo pozornej prostoty, jego dowód zajmuje w formie pisemnej dziesiątki stron. Kevin Buzzard z Imperial College London postawił sobie ambitny cel: przetłumaczyć te matematyczne zawiłości na język kodu komputerowego.
Do czego to służy? System o nazwie Lean to specjalny język, w którym komputery mogą weryfikować poprawność dowodów. Jeśli coś przejdzie przez „maszynę”, nie ma mowy o błędzie. Dotychczas w repozytorium Mathlib zgromadzono 2 miliony linii formalnej matematyki. Dzięki AI, te liczby rosną w oczach.
Problem „matematycznego szlamu”
Podczas ostatnich warsztatów naukowcy zauważyli zdumiewający skok wydajności. W ciągu zaledwie jednego dnia ilość napisanego kodu podwoiła się. Jednak praca z AI ma swoją ciemną stronę, którą naukowcy żartobliwie nazywają „warstwą szlamu”.
- Kod pisany przez AI jest często rozwlekły i niezdarny.
- Algorytmy używają nieoczywistych funkcji, które mogą przestać działać przy aktualizacji systemu.
- Gotowy dowód jest poprawny, ale dla człowieka bywa całkowicie nieczytelny.
Jak mówi Buzzard, budujemy na tym fundamenty, ale rodzi się pytanie: co stanie się, gdy spróbujemy dobudować kolejne piętro do tak chaotycznej konstrukcji? Czy system się zawali, czy pozwoli nam wejść na poziom matematyki, o której wcześniej mogliśmy tylko marzyć?
Czy AI nas zastąpi?
To nie jest już tylko kwestia technologii, ale filozofii. Jeśli maszyna udowodni twierdzenie, którego nie rozumie żaden człowiek, to czy naprawdę przyswoiliśmy nową wiedzę? Naukowcy tacy jak Hang Lu Su widzą w tym „uprzemysłowienie procesu intelektualnego”. Zamiast mozolnego wyprowadzania wzorów na papierze, badacze stają się operatorami potężnych modeli AI, zużywając tysiące funtów dziennie na moc obliczeniową.
Mimo wszystko, pasja pozostaje ludzka. Matematycy w Londynie nie przestają pracować, bo po prostu kochają ten proces. Czy jednak za 10 lat matematyka będzie jeszcze dziedziną ludzką, czy staniemy się tylko „kierownikami” procesów generowanych przez maszyny?
A jak wy sądzicie? Jeśli AI ostatecznie rozwiąże wszystkie wielkie zagadki matematyki, czy odkrycie to będzie dla nas równie wartościowe, co wynik pracy ludzkiego umysłu?
