Los postanowił uczynić ze mnie ofiarę swojej matematycznej ironii. Przez ostatnie 3 tygodnie nie byłem w stanie napisać ani słowa tutaj, ponieważ pochłonęła mnie bez reszty walka z pozornie banalnym problemem technicznym o roboczej nazwie "KawaNaŁyżeczce". Problem ten, choć z pozoru oczywisty niczym fakt, że nie da się napić kawy bez filiżanki (a przynajmniej bardzo trudno), wymagał udowodnienia formalnego w ramach struktury logicznej mojego nowego modelu iteracyjnego opartego na kontekstowej rekurencji dezorientacyjnej.
"KawaNaŁyżeczce" mówi mniej więcej tyle, że jeśli każdy z gości dostaje przynajmniej jedną łyżeczkę cukru, to łączna liczba łyżeczek nie będzie mniejsza niż liczba gości. Brzmi znajomo? Tak, to klasyczny przypadek "niby-wiadomo, ale spróbuj to udowodnić formalnie, kiedy twój system notacji sam pod sobą kopie dołki".
Planowałem rozwiązać to w jedno popołudnie. Skończyło się na trzech tygodniach ślęczenia, w trakcie których piłem więcej kawy niż moja struktura pojęciowa była w stanie przetworzyć.
Tak więc – przepraszam za brak aktywności. Po prostu byłem zbyt zajęty tłumaczeniem światu, że jeden plus jeden to naprawdę dwa, tylko że w moim świecie trzeba to najpierw aksjomatycznie udowodnić za pomocą 27-stronicowego lematu o nazwie "CukierNaGości".
Teraz kurwa frontendzi pojebani lazy loading na ikonkach, za moich czasów to się wszystkie wpierdalało w zipie na serwer i człowiek się cieszył jak się php nie wyjebał przy rozpakowaniu.
Są nowe wieści od pięknego umysłu.
Twierdzenie "FiNumSall" opisuje pewien względnie oczywisty fakt, który jest bardzo łatwy do uzasadnienia koncepcyjnego, słownego. Obrazowo, mówi on mniej więcej tyle, że jeśli ustawimy ileś skrzynek z butelkami, a w każdej skrzynce będzie co najmniej jedna butelka, to liczba butelek będzie większa lub równa liczbie skrzynek. Niestety udowodnienie tego faktu, umiejscowionego w formalnym opisie funkcji VMPC, zajęło mi 3 tygodnie intensywnej pracy. Przewidywałem, że zajmie mi to 1 dzień. Dowód tego niezwykle odkrywczego faktu zajmuje 1,5 strony A4.
Studentowi na 2 roku by to zajęło 45 minut na kolokwium poprawkowym, a ChatGPT 2 sekundy. 🧠
W idealnym świecie miałbym współpracowników, którzy komponowaliby takie dowody narzędziowe, a sam mógłbym się bardziej skupić na głównym torze rozumowania, jak te fakty ułożyć, aby ukończyć główny dowód, jednokierunkowości funkcji VMPC. Niestety wszystko muszę robić sam. To mniej więcej tak, jakby własnoręcznie jedna osoba budowała cały dom. Położyła cegły, instalacje, tynki, podłogi. Da się, ale zajmie to ogromną ilość wysiłku. Piszę to dla zobrazowania sytuacji, choć też dla złagodzenia własnej frustracji, na wypadek, gdyby ktoś zastanawiał się, jak to możliwe, że pisanie tego dowodu trwa tak długo.
xD
Kupiłem bilety na lot do Amsterdamu i dopiero teraz patrzę, że pojeby sobie liczą 1k za noc w Airbnb a ja jestem na 4 kurła. XD
