misterio

@fart To jest ogólnie ciekawe pytanie, czy w matematyce dowodowej będzie w stanie wyprzedzić ludzkość jako taką. Ogólnie są na ten temat dwa obozy, ale to może na kiedy indziej, bo to wpis na 10 stron.

@Hosh Tłumaczenie AI przez AI sprytnie.

Widzę, że w gorących "Politiken hattricken", więc dobry moment, żeby oderwać się od tego przez "matematiken". Ciekawostka, wczoraj opublikowano taki blueprint:

Może pokrótce wyjaśnię, o co chodzi. Ostatnie Twierdzenie Fermata (będę dalej posługiwał się skrótem - LFT), to szczególny przypadek pytania o rozwiązywalność dla konkretnego równania diofantycznego. Równania diofantyczne, to jak powinniśmy pamiętać ze szkoły średniej takie równania zdefiniowane w dziedzinie liczb całkowitych, które ogólnie można wyrazić jako f(x₁, x₂, x₃, ..., xₙ) = 0. Ujmując to prościej, są to takie równana, dla których odpowiedzią są co najmniej dwie zmienne. Na przykład a + 2b = 5 ma takie przykładowe rozwiązania jak (a=1, b=2) czy (a=3, b=1). LFT definiuje takie równanie: aⁿ + bⁿ = cⁿ jako nieposiadające żadnego rozwiązania (a, b, c) dla n ≥ 3. Dla n = 2 sprawa jest prosta, gdyż jak wiemy, takie rozwiązania muszą istnieć, bowiem są odpowiedzią wynikająca wprost z twierdzenia Pitagorasa. Na przykład (a = 3, b = 4, c = 5) i każde wielokrotności będą spełniać to równanie, więc jest ich nieskończenie wiele. Problem jednak komplikuje się, kiedy zwiększamy n. Przez stulecia udało się rozpatrywać różne przypadki, typu n=3, n=4, n=5 itd. Jednak każdy taki przypadek opisywany był innym typem dowodu, przez co nie dało się tego uogólnić na wszystkie liczby naturalne n. Dopiero w roku 1994 Andrew John Wiles opublikował dowód, zbierając całą wiedzę z przeszło 350 lat. Dowód ten jest bardzo mocno skomplikowany i można powiedzieć, że jest jednym z największych osiągnięć teorii liczb XXw. Zahacza on o wiele bardzo nowoczesnych konceptów z zakresu: geometrii algebraicznej, algebry Heckego, deformacji pierścieni, kategorii, schematów, czy krzywych eliptycznych.

Lean jest natomiast projektem, który ma w założeniach pozwolić wyrażać matematykę w sposób maszynowy. Ma to między innymi umożliwić AI rozumienie matematyki. Innymi słowy, nie chodzi o to, żeby AI była w stanie znaleźć dowód jakiegoś twierdzenia matematycznego w internecie i bezmyślnie go przeklepać pytającemu, czy wykonać jakieś algorytmicznie zdefiniowane obliczenie, typu obliczyć pochodną funkcji, tylko żeby faktycznie rozumiała pojęcia i formalizmy matematyczne, którymi operuje oraz zależności między nimi. Dzięki temu możliwym mogłoby być użycie AI do znajdywania odpowiedzi na do tej pory nierozwiązane problemy, co do których nie mamy wyrobionego "algorytmu postępowania".

W oparciu o Lean udało się stworzyć takie sztuczne inteligencje jak Lean AI, czy AlphaGeometry, które są w stanie rozwiązywać zadania matematyczne, które pierwszy raz "widzą na oczy" i nie mają dla nich wyrobionego schematu postępowania. AlphaGeometry udało się nawet uzyskać wydajność na poziomie złotego medalu Międzynarodowej Olimpiady Matematycznej, biorąc pod uwagę tylko zadania z geometrii. Powiedziałbym, że to małe oszustwo, ale byłoby to duże niedopowiedzenie, biorąc pod uwagę, że geometria Euklidesowa jak dowiódł Alfred Tarski, jest teorią spójną, kompletną i rozstrzygalną. Stety-niestety teoria liczb, do której domeny przynależy LFT, takową teorią nie jest, co niesie za sobą pewne implikacje. Możliwe, że jeszcze kiedyś popełnię coś na ten temat, jeżeli kogoś to interesuje.

O zamiarach sformalizowania LFT w Lean było już słychać pod koniec roku 2023, kiedy Kevin Buzzard dostał 5 letnie stypendium właśnie na ten cel, a dziś uzyskujemy końcowy rezultat? Niestety nic bardziej mylnego, tytuł tej pracy to niezły kilkbejt. Cała jest dostępna pod tym linkiem, więc jak kogoś interesuje, to proszę się częstować: https://imperialcollegelondon.github.io/FLT/blueprint.pdf
Natomiast w wielkim skrócie, to można powiedzieć, że nie widać nawet wierzchołka tej lodowej góry. Stwierdzone jest to pośrednio w 12 chapterze (appendix), jeżeli chodzi o twierdzenia zależne, które znane są ludzkości, ale nie istnieje ich formalizacja w Lean. Niektóre z nich to nadal wieloletni reaserch — co też stwierdza dokument.

Zatem czy AI będzie w najbliższym czasie pomocne w rozwiązaniu takich problemów, jak hipoteza Riemanna, czy problem Collatza? Mocno wątpliwe, na ten moment ludzkość jest znacznie bardziej rozwinięta pod kątem formalnej dowodowości matematycznej od jakiegokolwiek AI.

@don'T.R.I.P.e Filozoficzne pytanie brzmi: robić nic, czy nic nie robić.

@Toretto Ujmę to tak jeszcze. Jeżeli Kwaśniewski był szczytem w PL, to ja nie chcę wiedzieć, gdzie jest dolina, bo można by się nabawić depresji. Pun intended.

@Toretto Choć popieram w dużej części, co piszesz, to nie rozumiem, jak może Cię coś zaskakiwać. Nieironicznie duża część wskaże alkoholika-komunistę jako najlepszego prezydenta RP w historii po PRL. Ten urząd jest ośmieszany co kadencję od 35 lat przez najróżniejsze opcje polityczne, czy jeden gość z powiązaniami z półświatka coś zmieni?

@partymaker Ja widzę Modrica, Kroosa i Góralskiego.

@Roobo Nie wiem, czy bardziej przeraża to, czy podstawowe wykształcenie z 50+% na Nawrockiego. Jak w tym kraju ma być dobrze.

@Kgorecki2500 Dobra, odstawiam animce na tydzień-dwa, bo zastanawiałem się dobre 3 minuty, co japoński zwrot zdrabniający robi przy potężnym Duńczyku.

@NeroTFP1 Kto się pierwszy odezwie przegrywa, lata 90.

@GTBTP To fakt, ale było 10 vs 0,5 xD

Bawi, że jednak mijanka Zandberga z Hołownią. Pączki nie pomogły.

@MesQueUnClub96 A to dopiero początek ośmieszania tego urzędu. Od 35 lat.

Przegraliśmy ostatni mecz u siebie. Niestety, zły prognostyk na przyszły sezon, aby nie powiedzieć fatalny. Klub należy zlicytować. Fabian ostatecznie wygrał.

Bramkarz potrzebny na już, czy bez szans w sytuacjach? Zapraszam do dyskusji.

@Kapitan hawk Ostatni w tym sezonie, tak ogólnie to byłbym sceptyczny ;)

@FCBparasiempre Generalnie jeszcze post raz na jakiś czas na inny temat spoko, ale to jest dosłownie ściana bzdur, która się przewija kilometr. W zasadzie koncepcyjnie nie wiem, czym to się różni, że potrafią jeden za długi wpis usunąć, ale 500 na ten sam temat, które przewijasz jeszcze dłużej, są już OK.

@Kgorecki2500 Tak szczerze to przekaz tego jest 12/10 biorąc pod uwagę, jakie płytkie gunwo jest serwowane na tym festiwalu.

@Luciano99 Nie powinno, to być tyle materii barionowej we Wszechświecie zakładając symetrię między nią a antymaterią. Reszta to już tylko następstwa.

@MessiForeverTheBest Ciekawe w sumie co by się stało, gdyby kiedyś doszło do sytuacji, że każdy, kto, wypełniając AML-kę zaznacza, że nie jest PEP-em, ani nikt z jego rodziny nie poszedł. W sensie, jaka wtedy byłaby frekwencja.

Zapewne nadal byłby to ważne wybory, ale na świecie chyba nie przeszłyby bez echa, bo prawdopodobnie byłby to wynik jednocyfrowy.

@Criss18Barca @kulek22 Ja dla pewności otworzyłem własny lokal wyborczy z komisją.

Wychodzi na to, że etat szkodzi jak 24 fajki dziennie:

https://imgflip.com/i/9udr62

@NeroTFP1 Co sobie ludzie pobredzili o spisku jury, to ich.

Naszła mnie taka rozkmina. Myślicie, że @Moderacja jutro rano musi to wszystko przejrzeć pod kątem potencjalnej agitacji? Jeżeli tak, to współczuję i tu nawet nie chodzi o ilość...

Jest przedsmak tego, co będzie się działo jutro – przaśnie. Edit w sumie to już dziś. Żyć nie umierać.

@szkudi7 Że w pracy nie ma przyjaciół, są tylko znajomi.

@Bilon87 A sprawa trafiła do płokułatuły.

@LeoMessiiBarcaPepa Po czasie idzie się przyzwyczaić.

@Commando

Trzeba uważać, komu dajecie zielone.
https://x.com/niebezpiecznik/status/1923799610994078158