Anons: nowy numer "Notices of the AMS" o dowodach formalnych

Jako sie rzekło w tytule, najnowszy numer szczęśliwie dostępnego w internecie za darmo, czasopisma "Notices of the AMS" poświęcony jest formalnym i wspomaganym maszynowo systemom dowodzenia twierdzeń. Jakoś tak się złożyło, że jest to interesujące postscriptum do miłej pogawędki jaką parę miesięcy temu odbyła się tu. Można formalizację lubić, cenić, bądź uważać ją za płochą igraszkę czy wręcz perwersję intelektualną. Jednakże, kiedy się zastanowić i zdać sobie sprawę jak skomplikowany jest gmach matematyki, jak rośnie, można też wyobrazić sobie pewien rodzaj niepokoju, czy natręctwa jakie dręczy wielu matematyków, że gdzieś w jego środku tkwi jakiś błąd. Opisane w Notices metody to swoista terapia, ale i być może punkt wyjścia do matematyki przyszłości.
Oczywiście metody formalne wychodza poza matematykę. Bezawaryjny hardware czy software jest kluczem w wielkich przedsięwzięciach których stawką są ogromne pieniądze, życie ludzkie, środowisko naturalne. Wyniki badań nad formalnym wspomaganiem dowodzenia użyte do weryfikacji poprawności programów (każdy z nich jest przecież czymś w rodzaju teorii matematycznej) to być może jedyna droga by znaleźć tego Graala.
Co ciekawe wśród projektów tego typu - ładny akcent polski. Poczesne miejsce wśród nich zajmuje rozwijany od lat siedemdziesiątych w środowisku matematyków związanych a Uniwersytetem Warszawskim i Uniwersytetem w Białymstoku, ale w istocie będącym projektem międzynarodowym - system Mizar.
Mam i inne skojarzenie (też trochę szowinistyczne) a może i wspomnienie. Systemy weryfikacji twierdzeń opierają się na ciekawych systemach podstaw matematyki, konkurencyjnych w stosunku do teorii mnogości ZFC i lepiej od niej przystosowanych do "zmechanizowania". Ciekawe w tym kontekście wydaje mi się przeanalizowanie potencjału zapomnianych już dziś ale wielce oryginalnych systemów Leśniewskiego: prototetyki, ontologii i mereologii. W pewnym okresie swej pracy zawodowej (dawno dawno temu w odległej galaktyce) odbywałem dyskusję na temat ich potencjalnej przydatności w świecie komputerów. Niestety - wówczas też przyszedł kryzys, inwestorom zabrakło pieniędzy i wiary, fima splajtowała spektakularnie, a mnie potem zabrakło zapału i samozaparcia, żeby poważnie się ich nauczyć i rozwinąć nieśmiałe pomysły.

Zdjęcie: mimikra

Frog ?, originally uploaded by minthem.

Mimikra jest bronią. Bronią drapieżników i bronią słabych. Polega na wtopieniu się w tło, ukryciu swej obecności, upodobnieniu się do otoczenia. Drapieżnik nie chce by dostrzegła go ofiara. Słaby, nie chce zwrócić uwagi silnego.
Drapieżnikom wybacza się mimikrę. Jakoś tak nasza kultura po cichu czci silnych - rozgrzesza ich sukces.
Mimikrę słabych spotyka potępienie, a przynajmniej pogarda. Kiedy znikają prawdziwe drapieżniki, ich czas się skończył, pojawia się klasa stworzeń, którą zaklasyfikowałbym jako mendy. Z jedynej broni jaka dostępna była tym, którzy nie mają kłów, pazurów, szybkich jak wiatr nóg, pancerza czy trującego żądła czynią przedmiot drwiny. Szyderstwo, lub dzikie egzorcyzmy - to sposób działania mend. Pogardą zamiast atramentem spływają ich pióra, pogarda bije z ekranów telewizyjnych, pogarda wybrzmiewa gdy skończą każde zdanie.
Słabość jednych w czasie próby to dowód słabości w ogóle. W tej pogardzie czuć strach przed własną słabością, przed istnieniem słabości w ogóle. Czuć też ponury rytuał walki o władze nad stadem. Mendy powoli zamieniają się w drapieżniki.
Jeżeli postawią na swoim, słabym nie pozostanie nic innego jak mimikra.

Mgła

Mgła spowiła Kraków. Właściwie jedno z moich pierwszych wspomnień z tego miasta to żółto-pomarańczowe światło latarni otulone kłębem mgły. Teraz jest tak samo. Niemal dwadzieścia lat później. Z niewiadomych przyczyn wstałem dziś o 4:30. Snułem się po domu, próbowałem zmusić mój aparat do zrobienia sensownego zdjęcia, czytałem, pisałem, liczyłem, parzyłem kawę żonie, żeby przygotować jej milsze niż zwykle przebudzenie. Potem podróż 114-ką przez białoszary kłąb, który trochę tylko się rozjaśnił - trochę matematyki w autobusie. Szkoda tej niemal godziny na głupie patrzenie się w okno albo przysłuchiwanie się szczebiotaniu studentek jadących na kampus... Praca. Cholera, jak to jest - czasem nic się tam nie dzieje, a czasem po prostu nie można się połapać w natłoku zajęć. Powrót - nadranne wstawanie odbiło się jednak: mało matematyki i nieskuteczna walka z lekką drzemką. W telewizji w kółko o wyborach: gdzieś daleko. Niech zgadnę jak głosują moi znajomi w których kubikach powieszone były rysunkowe żarty z GWB. Mgła nadal stanowi dominantę. Dopada mnie spleen. A może po prostu jestem śpiący ?
P.S. Ruszyłem z projektem o którym wspominałem. Początek powolny ale i całe tempo będzie takie: CFGDA

Projekt CFG-DA

Mam zamiar rozpocząć na osobnym blogu publikację w maleńkich porcjach polskiego tłumaczenia sławetnej książki "Disquisitiones Arithmeticae" Carla Friedricha Gaussa.
Po co? Z kilku powodów.
Po pierwsze, od dawna chodzi mi to po głowie, więc czas zacząć działać.
Po drugie, skandalem jest, że ta książka jak zresztą wiele innych fundamentalnych i historycznie ważnych nigdy na polski nie została przetłumaczona. Wstyd dla całego naszego środowiska naukowego i nie tylko.
Po trzecie i tak tą książkę czytam, więc tłumaczenie nie będzie jakimś wielkim problemem.
Po czwarte (tu rodzi się pytanie, po co tłumaczyć tak stare książki) DA jest w jakimś sensie wciąż żywa. Nie jest niezwykłe we współczesnych pracach z teorii liczb znaleźć odniesienia do poszczególnych artykułów z DA - to ziarno zaowocowało wspaniałym drzewem. Nawet, gdyby odniesienia były tylko natury czysto historycznej - nie najgorsze to zajęcie poznawanie myśli ludzkiej w różnych fazach jej rozwoju na spędzenie jakoś czasu zanim nadejdzie nasz kres. Ale mam wrażenie, że odniesienie do DA polegają współcześnie również na tym, że myśl Gaussa jest wciąż inspirująca. Że w tych dociekaniach młodego geniuszu, pisanych jak mi się wydaje tyleż dla innych co dla siebie samego, w tych wytrychach i fortelach jest nauka wciąż aktualna a patyny dwóch wieków (publikacja DA to 1801 rok) poza nieco archaicznym stylem (o czym za chwilę) praktycznie nie widać.
Po piąte mam wrażenie że DA posiada wielkie walory edukacyjne. Sądzę, że w młodości, w czasach kiedym chodził do liceum byłoby z wielkim pożytkiem dla mnie gdyby ktoś mi tą książkę pokazał.

Tyle o powodach. Mam kilka problemów, które muszę jakoś rozwiązać. Pierwszy natury technicznej. Najbardziej, ze względu na wygodę jest mi publikować w formie bloga. Ale książka jest w jakimś sensie odwrotnością bloga jeśli chodzi o układ typograficzny. Czytanie blogu zaczyna się "od góry", od najświeższego wpisu, w książce zaś "na górze" są jej wcześniejsze części. Pozornie niewielka zmiana wprowadza trochę zamieszania. Zwroty typu "poniżej" odnoszące się w książce do do tekstu późniejszego jeśli wychodzą poza zakres jednego wpisu na blogu tracą trochę sens. Tym niemniej, żeby uniknąć niepotrzebnych komplikacji będę się posługiwał "porządkiem książkowym" licząc, że jeśli ktoś zrozumie rozważania Gaussa z łatwością uwzględni w czytaniu ową drobną formalną niekonsekwencję.
Drugi problem jest o wiele poważniejszy. Gauss napisał DA po łacinie - w języku, którego nie znam. Tłumaczył więc będę z angielskiego tłumaczenia Arthur'a A.Clarke. To rodzi serię "subproblemów". Po pierwsze ufam temu, że pan Clark (w zasadzie powinienem powiedzieć ojciec Clark, bo to jezuita) zachował styl oryginału i tegoż będę się trzymał. Po drugie i co ważniejsze, nie jest dla mnie jasny status praw autorskich w takiej sytuacji. Nie chcąc być piratem i narażać się na posądzenie przez właściciela praw autorskich do tłumaczenia angielskiego o zabieranie mu potencjalnych zysków z publikacji polskiej, póki co uczynię bloga dostępnym imiennie tylko na wyraźne żądanie PT czytelników. Kiedy wyjaśnię kwestię prawną, jeśli będzie to możliwe upublicznię bloga. Póki co nazwijmy to "głośnym czytaniem" DA.
Zatem, aby zapisać się jako czytelnik "CFG DA" należy zgłosić taką chęć w komentarzu do niniejszego posta podając swój adres pocztowy względnie wysłać prośbę na adres poplawski.artur@gmail.com. Za niedogodność przepraszam, mam nadzieję, że to co napisałem stanowi dobre usprawiedliwienie.
Wielką zaletą DA jest jej podział na 365 artykułów (sądzę, że zbieżność tej liczby z ilością dni w roku nie jest przypadkowa). To daje naturalny podział na kwanty w jakich postaram się publikować tłumaczenie. Wadą na początku będzie zapewne to, że przez pierwszych kilka artykułów niewiele będzie się działo, natomiast później porcja wydaje się dobrze dostosowana do rozważenia w ciągu jednego dnia. Mnie natomiast ułatwi to znakomicie dostosowanie tempa publikacji do różnych wahań w zasobach wolnego czasu na pisanie.
Początek publikacji z pewnych względów planuję na poniedziałek 3-go listopada. Zapraszam do wspólnego czytania, wspólnej nauki i świetnej zabawy umysłowej. Mam nadzieję, że wspólnie wytrwamy.