Debiut Tricki

Parę godzin temu pojawił się anons, że strona o której już tu jakiś czas temu pisałem jest aktywna i dostępna dla użytkowników. Chodzi o projekt "Tricki" - czegoś rodzaju wiki tyle, że z opisem sposobów, sztuczek, wytrychów, metod itd. które można zastosować w pracy matematyka. To wyjątkowy pomysł - nie monografia, nie encyklopedia, nie wykład. To nauka warsztatu. Bezcenna sprawa. Pomysł sygnują i kontrybuują do projektu wybitni matematycy współcześni, w tym laureaci medalu Fieldsa: Timothy Gowers i Terence Tao.
Polecam - sam już oblizuję się na myśl czego się można już i czego się można będzie w przyszłości z materiałów tam zamieszczonych nauczyć.
Szczególnie polecam tej, bliskiej mi mentalnie grupie ludzi (której istnienie i liczność przekraczającą jeden na nikłych przesłankach antycypuję), którzy zdobyli formalne wykształcenie matematyczne (lub pokrewne) i matematyką się interesują "twórczo", tzn. lubią popracować nad jakimś problemem, a z różnych przyczyn znaleźli się poza szeroko rozumianym środowiskiem akademickim. Internet, a szczególnie takie inicjatywy to wielka szansa dla nas, aby nie stracić kontaktu z prawdziwą nauką. Szkoda tylko, że w polskojęzycznym Internecie tak mało się w owym światku dzieje.

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.

Anons: Ruch na blogach. Tricki. Knol.

Profesor Timothy Gowers na swoim blogu zaanonsował dzisiaj powstanie Tricki - nowego narzędzia, działającego na zasadzie podobnej do wiki, gdzie będzie można znaleźć i publikować różnego rodzaju sztuczki, kruczki, metody i wzorce stosowalne w rozumowaniach matematycznych.
To wspaniała idea która wzbudziła sporo zainteresowania na pronumerowanych przeze mnie blogach. Mam po cichu nadzieję, że jeśli chwyci, może być dla matematyki nieocenionym a może i przełomowym momentem. Może stać się tym czym skatalogowanie "design patterns" stało się dla inżynierii oprogramowania. Jakkolwiek tautologicznie by to nie zabrzmiało, być może wkraczamy w okres "matematyki opartej na wiedzy", przez analogię do gospodarki opartej na wiedzy.
Gorąco kibicuję, czekam i będę zawzięcie studiował, do czego zachęcam i innych. Kilka wprawek jakie pojawiły się na blogu Timothy'ego Gowers'a i innych wygląda bardzo obiecująco.

Skoro już na anonse mi się zebrało, polecam knolową serię Włodka Holsztyńskiego. Również wygląda bardzo obiecująco. Również polecam.