Я, конечно, не математик и, наверное, зря подозреваю людей, го | Микола Канян

Я, конечно, не математик и, наверное, зря подозреваю людей, гораздо более умных, чем я. С юных лет у меня были проблемы с математикой. Помимо прочего, оттого, что любое более-менее сложное математическое доказательство всегда вызывало у меня много глупых вопросов. Сильной т.н. "математической интуиции", столь необходимой в таких случаях, я так и не выработал.

Наверное, именно поэтому меня так заинтересовала теория типов и построенные на ней системы интерактивного доказательства теорем. Там, если непонятно, что значит какая-то закорючка, можно на нее нажать и увидеть. А если сделал логическую ошибку в выражении, оно само выделяется красненьким. Я недостаточно умен, чтобы быть математиком и работать только карандашом и бумагой.