schegloff (schegloff) wrote,
schegloff
schegloff

Любопытное совпадение

Как вы наверное помните, идея заняться математикой как языком программирования пришла мне в голову буквально на днях, в августе 2016. Казалось бы, остальное человечество, и входящие в его число математики, должны были сообразить то же самое значительно раньше, и давно уже переделать математику в 146% техническую дисциплину. Тем более, что необходимость этого известна уже давно:

Много веков что математические доказательства, что математические построения (как в геометрии: помните, там часто достраивают всякие штуки, чтобы доказательство провести) записывали обычными человеческими словами. В 19ом веке случился кризис, стало понятно, что если доказательства записывать недостаточно строго, возможны очень тонкие ошибки, которые очень тяжело заметить.

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

Идеи на эту тему были уже у Декарта и Лейбница, но первая попытка сделать такой язык и такую систему принадлежит Фреге с его Begriffschrift...


Однако выяснилось, что к решению этой задачи математики приблизились лишь совсем недавно, да и то далеко не все:

...мне удалось создать унивалентный подход к формализации, который позволяет использовать программную оболочку UniMath для того, чтобы записывать те утверждения, которые мне нужны. Сейчас я могу запросто записать лемму и проверить ее доказательство, у меня есть этот язык. Точнее, язык был давно - он называется Coq, но теперь я знаю, как его использовать для решения математических задач.
- Как все же родилась UniMath?
- Ее ядро - мои Foundations и еще несколько библиотек, которые использовали “основания” в качестве базиса. Я был инициатором всего этого, потом привлек к работе нескольких людей. Сегодня в команде Unimath Development Team четыре человека. Помимо меня это Бенедикт Аренс, Даниэл Грейсон и Майкл Уоррен. Само название UniMath года полтора назад подсказал Дэн Грейсон.
- Вы же не специалист в программировании, а здесь наверняка приходилось писать коды, программы.
- Кстати, я умею писать программы. Когда-то на первом курсе мехмата я подрабатывал, преподавая программирование. Так что в этой области я себя чувствую комфортно. Но практически мне этого делать не пришлось, потому что я задействовал готовую систему Coq, которая к тому времени существовала лет 20... Она очень общая, ее можно применять для многих целей. В том числе для того, чтобы проверять логические манипуляции. Оттолкнувшись от нее, я придумал новый стиль ее использования, новый способ записывать математику.
- А вы можете сказать: разработанная мною программа уже позволила мне сделать то-то и то-то? Или вы продолжаете работать над совершенствованием системы UniMath, и это сегодня основная ваша задача?
- Я сейчас продолжаю заниматься не столько даже совершенствованием UniMath, сколько тем, чтобы убедить математиков, что способу использования компьютерной системы, который я придумал, действительно можно доверять. То есть если система говорит, что доказательство правильное, то оно действительно правильное. Это неочевидно, в этом надо людей убедить.


Так что не успел я даже собраться поизучать математику - а уже оказался впереди паровоза :)
Tags: математика
Subscribe
  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 37 comments