Grigori Mints

Grigori Mints, ka Grisha Mints (vene keeles Григорий Эфраимович Минц; 7. juuni 1939 Leningrad – 29. mai 2014 Palo Alto, California) oli Nõukogude Liidu ja Ameerika Ühendriikide loogik, arvutiteadlane ja matemaatik.
Grigori Mints oli rahvusvaheliselt tuntud loogik ja arvutiteadlane, kelle tööd tõestusteoorias on leidnud otsest rakendust arvutiteaduses. Ta on jätnud olulise jälje Eesti arvutiteadusesse. Tema õpilased on Tallinna Tehnikaülikooli professor Tanel Tammet ja akadeemik Tarmo Uustalu.
Ta oli Stanfordi Ülikooli professor ja Eesti Teaduste Akadeemia välisliige.

Haridustee

Grigori Mints lõpetas 1961. aastal Leningradi Riikliku Ülikooli matemaatika erialal ning kaitses 1965. aastal sama ülikooli juures füüsika-matemaatikakandidaadi ja 1990. aastal füüsika-matemaatikadoktori kraadi (doktoriväitekiri "Преобразования доказательств и синтез программ").

Enne Eestit

Aastatel 1961–1979 töötas Grigori Mints vanemlaborandi ja nooremteadurina NSV Liidu TA V. A. Steklovi nimelise Matemaatika Instituudi Leningradi osakonnas. Ühtlasi töötas ta aastatel 1962–1979 Leningradi Riiklikus Ülikoolis, kus luges põhiosa loogikakursustest.
Tema teaduslikud huvid haarasid matemaatilist loogikat (põhirõhuga tõestusteoorial), asendusmeetodit, dünaamilist topoloogilist loogikat, konstruktiivset matemaatikat. Grigori Mints kuulus Leningradi tõestuste teooria koolkonda. Koos kolleegidega lõi ta klassikalise loogika tarbeks tõestuse otsingu strateegiad ja nende rakendamise programmid, sealhulgas esimese loomuliku keele kasutajaliidesel põhineva loomuliku tuletamise programmi (1964).

Eestis

Grigori Mintsi lähem kokkupuude Eesti teadusega sai alguse 1970. aastate lõpul, mil ta esines Tartu Riikliku Ülikooli programmeerimise kateedri ja Teaduste Akadeemia Küberneetika Instituudi ühises suvekoolis Pärnu lähedal Elbis. Loengute teemaks oli algoritmide ajaline keerukus. Kuid 1981. aastal asus ta juba elama ja tööle Eestisse, kus ta oli aastatel 1981–1991 TA Küberneetika Instituudi vanemteadur.
Grigori Mints ja Tanel Tammet leidsid ja realiseerisid koostöös uued tõestusvõtted teoreemide automaatseks tõestamiseks klassikalise loogika raames. Tõestusteooria-alased uurimused on leidnud rakendust arvutiteaduses, sealhulgas ka Eestis loodud programmeerimissüsteemides PRIZ ja NUT.
Mints on teinud koostööd ka Enn Tõugu töögrupiga – koos töötasid nad välja arvutusmudelite ja programmide sünteesi formaalloogilised esitused, mis pakkusid suurt huvi loogikutele.
Mintsi Küberneetika Instituudi perioodi tegemiste haare oli suur – kolleegidele loogika tõdede õpetamine, uurimisprojektides osalemine, programmide sünteesi loogilisi aluseid selgitava trükise avaldamine, loengute pidamine, teadusürituste korraldamine, ja rahvusvaheliste teaduskontaktide edendamine. Tema õpilased on Tanel Tammet, hilisem Tallinna Tehnikaülikooli professor ja Tarmo Uustalu, hilisem Eesti TA akadeemik.
1991. aastal töötas Mints lühemat aega osakoormusega professorina Tartu Riikliku Ülikooli programmeerimise kateedris, kus ta luges tõestuste teooria kursust.

Pärast Eestit

1991. aastal valiti Grigori Mints Stanfordi Ülikooli professoriks filosoofia alal. Hiljem lisandusid samas ülikoolis veel arvutiteaduse (1992) ja matemaatika professori ametikohustused (1997).
Grigori Mints on töötanud külalisprofessorina tippülikoolides, nagu Kuninglik tehnikaülikool Stockholmis, California Ülikool Berkeleys, Müncheni ülikool kui ka nõustajana Californias Palo Altos asuvas Kestreli Instituudis. Ta oli paljude doktoriväitekirjade juhendaja. Tema sulest on ilmunud üle kolme tuhande retsensiooni tuntud referaatajakirjadele, sealhulgas Mathematical Reviews, Zentralblatt für Mathematik, Computer Abstracts ja Referativnõi Žurnal : Matematika ("Реферативный Журнал : Математика").
2009. aastal külastas Mints Venemaa TA Steklovi-nimelise matemaatika instituudi Peterburi osakonna matemaatilise loogika laboratooriumi. Viiepäevast USA teadlase teadusvisiiti finantseeris Dmitri Zimini Fond Dünastia programmi "Välisteadlaste lühiajalised visiidid Venemaale" raames.