О людях с техническими мозгами

[minski_gaon]

Comments

[nekto_aip]

Автор, блогер.
Смысл, пусть каждый поставит сам.

[f_l_o_e]

Какая дикая гуманитарная чушь.

[antshadow]

Нет, автор молодец.

[antshadow]

Неожиданно хороший обзор! 99% сказанного на эти темы - пошлятина беспомощная, а тут... Браво, автор.

[admiral_hood]

А тут всего 70%

[antshadow]

А тут - Абсолютная Истина Как Она Есть.

[admiral_hood]

Как она есть, пьёть и спить

[aafin]

"А по-моему, ты говно"

[formerchild]

Троллей забыли. Это такая разновидность виртуозных логиков, бескорыстно двигающих науку. ))) Живут и здравствуют. Их все знают и любят.

[minski_gaon]

ну да, чуток протроллил ))

[minski_gaon]

Но Вы как математик все равно понимаете, я надеюсь, что логически математику до конца формализовать нельзя. Логические пруф чекеры для топовых мат терем построить не возможно.

И это, кстати, интересная задача -- формализация математики каким-то одним языком, который наверняка не будет стандартным языком мат логики

[formerchild]

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