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