Viena nianse, kuru vakarnakt nepieminēju. Katrs pierādījumu asistents lieto savu valodu (tipu rēķinus). Un dažkārt matemātika ir tik jauna, ka vajadzīgi jauni tipu rēķini, valoda un pierādījumu asistenti. Tagad tas notiek HoTT un univalentā matemātikā un ar laiku var būt vēl. Un tur cilvēka supervīzija MI nepieciešama math automatizācijā. Bet es priekš sevis arī esmu izdomājis automatizācijas shēmas arī šajā gadījumā, tāpēc to neminēju. Bet, jā. Šāda problēma pastāv.