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

[minski_gaon]

Comments

[formerchild]

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

[minski_gaon]

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

[minski_gaon]

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

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

[formerchild]

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

[minski_gaon]

будем посмотреть.

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

[formerchild]

TT вообще и HoTT в частности - это отказ от теории множеств, по сути. Альтернатива.

[minski_gaon]

Да. И в этом есть перспектива. Вообще идеально создать что-то вроде языка программирования для всей математики, может на базе ТТ

[formerchild]

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

[minski_gaon]

круто! Вот лучше делать на основе программирования.

[formerchild]

Ну как бы TT это тоже на основе программирования. Там все завязано на Curry-Howard correspondence, которое связывает программирование с логикой, отображает их друг в друга.

[formerchild]

Может потому, что "топовая" теорема развивает логику? Вносит новые правила в игру?

[minski_gaon]

да, именно, там всегда соединение несоединимого, поэтому логика буксует. Как один знакомый показал идентичность одного из расширений клеточных автоматов до решения дифур. Это не публикуемо, но если он посидит и сделает теорему -- будет очень даже интересно.

[formerchild]

Этот пример доказуем современными пруф-чекерами. Зависит от математической культуры.

[minski_gaon]

этот да, раз завязано на автоматах. Но вот Проблема Пуанкаре, решенная Перельманом?

[formerchild]

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

[minski_gaon]

Идеально, доказательство должна проверять машина, а не 10 человек в мире. Но до этого еще очень далеко.