3 czerwca 2015 r. na Wydziale Matematyki i Informatyki Uniwersytetu w Białymstoku Yasushige Watase, matematyk z Tokio, odbierze nagrodę “Mizar Prize for young researchers 2014” za swój artykuł “Lagrange’s Four-Square Theorem”.

Nagroda w wysokości 1000 Euro jest przyznawana przez Association of Mizar Users. Są do niej nominowani młodzi naukowcy z różnych krajów, międzynarodowe jury nagrody przyznaje ją pod koniec każdego roku.

Association of Mizar Users to niezależna, międzynarodowa organizacja skupiająca użytkowników systemu Mizar. Jego budowę rozpoczął w 1973 roku dr Andrzej Trybulec, polski matematyk i informatyk związany przez wiele lat z Uniwersytetem w Białymstoku. Jest jednym z największych osiągnięć naukowych białostockiej uczelni w dziedzinie matematyki i informatyki. Dziś system jest rozwijany nie tylko na UwB, ale także na Uniwersytecie w Nijmegen (Holandia) i na Uniwersytecie Shinshu (Japonia).

System MIZAR jest wytworem typowo polskim, odwołującym się do zapoczątkowanej jeszcze w okresie międzywojennym polskiej tradycji badań logicznych. Jego ideą było dostosowanie języka dowodzenia matematycznego do rozwoju technologii, tak by formalny zapis matematycznych twierdzeń i dowodów był zrozumiały także dla komputerów, które mogą następnie dokonać ich sprawdzenia.
Taka forma weryfikacji jest bowiem pewniejsza, niż wtedy, gdy pracę matematyka analizuje jedynie człowiek. Komputer skuteczniej wyłapuje uproszczenia zapisu czy ewentualne błędy w dowodach.
System sprawdza się też w dydaktyce, do nauczania dowodzenia matematycznego. Bywa, że jest wykorzystywany przy pisaniu prac magisterskich czy doktorskich. W Polsce – to jeszcze dość rzadkie zastosowanie, ale np. w Japonii taka forma zapisu prac młodych matematyków jest bardzo powszechna.

Sprawdzone przez system Mizar dowody matematyczne trafiają do specjalnie stworzonej bazy - Mizar Mathematical Library (MML). To unikalne repozytorium matematyki formalnej. Co ciekawe, system pozwala też potem przetłumaczyć zapisane w nim językiem formalnym teksty na język naturalny. Artykuły są publikowane w czasopiśmie Formalized Mathematics – jednym z dwóch na świecie czasopism publikujących artykuły matematyki formalnej, którego redaktorem naczelnym jest dr Roman Matuszewski z Uniwersytetu w Białymstoku. To właśnie najlepsi autorzy artykułów są nagradzani nagrodą “Mizar Prize for young researchers”.

W tym roku wręczenie nagrody odbędzie się podczas pobytu w Białymstoku prof. Włodzimierza Kuperberga z Uniwersytetu w Auburn (Alabama, USA). Jest on jednym z fundatorów nagrody. Na Uniwersytecie w Białymstoku wygłosi wykład nt. „Aproksymacja obszarów wypukłych płaskich przez wielokąty wpisane i opisane”. Spotkanie jest otwarte dla wszystkich zainteresowanych. Rozpocznie się o godzinie 14:15 w siedzibie Wydziału Matematyki i Informatyki UwB w nowym kampusie, sala 2048.

Za:rzecznik UwB