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.