
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".