Официально


Минобрнауки проводит отбор на 2020/2021 учебный год федеральных государственных образовательных организаций, на подготовительных отделениях и факультетах которых иностранцы и лица без гражданства, поступающие на обучение в пределах соответствующей квоты, будут иметь право на обучение по дополнительным общеобразовательным программам, которые помогут им подготовиться к освоению профессиональных образовательных программ на русском языке, за счет бюджетных ассигнований.



Госслужащий обязан незамедлительно уведомлять представителя нанимателя обо всех случаях обращения к нему каких-либо лиц, склоняющих его к коррупционным действиям. Такая норма предусмотрена в приказе Минпросвещения «Об утверждении Порядка уведомления представителя нанимателя (работодателя) о фактах обращения в целях склонения федерального государственного гражданского служащего Министерства просвещения РФ к совершению коррупционных правонарушений», который зарегистрировал Минюст.



Министерство науки и высшего образования опубликовало План деятельности на период с 2019-го по 2024 годы. Документ доступен на сайте ведомства.



Федеральная служба по надзору в сфере образования и науки «за неисполнение предписания в установленный срок» запретила прием в Московскую богословскую семинарию евангельских христиан-баптистов.






Новости № 7(2019)

Регионы


СНГ


Интердайджест


Получены новые данные о влиянии бактерий кишечника на настроение и их способности предотвращать депрессию. С подробностями - Sciencemag.org.

Находка обнаружена в ранее неизвестной семейной гробнице эпохи Птолемеев. Об этом рассказывает New York Times.

Изобретена таблетка с иглой для уколов внутри организма. Новость распространили MIT News; Science News.























Виден выход из норы. Труд математиков можно облегчить.
Наука
№ 38(2015)

18.09.2015

Владимир Воеводский - человек в научных кругах заметный и знаменитый: Филдсовский лауреат, единственный профессор с российскими корнями в престижном Институте перспективных исследований (Institute for Advanced Study) в Принстоне (США), несколько лет занимается разработкой нового научного направления, которое, по его убеждению, может принести огромную пользу математическому сообществу. В интервью корреспонденту “Поиска” четырехлетней давности Владимир Воеводский рассказывал о работе над “основаниями математики” (“Foundations”), а в конце августа приехал на Форум лауреатов в Гейдельберг с лекцией о готовой программной оболочке UniMath, которая представляет собой формализованную библиотеку математических определений и теорем и по сути является той самой “палочкой-выручалочкой” для его коллег. О деталях работы мы и расспросили ученого.

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

Беседовала
Светлана Беляева
Фото автора


 

Отзывы

Чтобы оставить отзыв необходимо авторизоваться или зарегистрироваться



 

Статьи на тему

Суммируя ряды. Демидовские лауреаты вдохновляют молодых ученых.
В зале торжественных заседаний Уральского федерального университета, оформленном портретами лауреатов премии, прошли традиционные Демидовские чтения. /№ 7(2019)
От тривиального к недоступному
Демидовский лауреат в номинации «Математика и механика», вице-президент РАН и академик-секретарь Отделения математических наук Валерий КОЗЛОВ в разных своих ипостасях он неоднократно давал газете интервью, комментировал актуальные события... /№ 7(2019)
Связать в единое
Демидовский лауреат академик В.Минкин - один из самых цитируемых российских ученых... /№ 7(2019)

Новости


Российские студенческие отряды отметили 17 февраля свой официальный праздник.



Международные рабочие комиссии по сотрудничеству в рамках научных и образовательных "дорожных карт" между Россией, Францией и Германией будут сформированы в апреле 2019 года, сообщил ТАСС министр науки и высшего образования Михаил Котюков.



Создание научно-технологических центров будет способствовать достижению целей, которые поставлены в рамках нацпроекта «Наука», заявил министр науки и высшего образования Михаил Котюков на сессии «Инновационные научно-технологические центры. Какими они будут» Российского инвестиционного форума в Сочи.



На встрече с главами регионов в рамках Российского инвестиционного форума в Сочи премьер-министр Дмитрий Медведев заявил, что, участвуя в реализации нацпроекта «Образование», региональные власти должны рассчитывать не только на федеральные средства, но и на привлекать частных инвесторов.



В Минобрнауки не поддерживают идею о введении запрета на выезд из страны для молодых ученых, сообщил «Интерфаксу» министр Михаил Котюков.



Совет научной молодежи Сибирского отделения РАН обратился к Владимиру Путину с открытым письмом по поводу инициативы правительства лишить Сибирское отделение РАН права оперативного управления имуществом и землями Новосибирского научного центра.



Строительство источника синхротронного излучения СКИФ начнется в Новосибирске в 2021 году, сообщил в интервью ТАСС на Российском инвестиционном форуме в Сочи губернатор Новосибирской области Андрей Травников.



Конференции


С 28 по 30 мая 2019 года в Центральном институте авиационного моторостроения имени П.И. Баранова (ЦИАМ, входит в НИЦ «Институт имени Н.Е. Жуковского) состоится Всероссийская научно-техническая конференция молодых ученых и специалистов «Авиационные двигатели и силовые установки».

Центр научно-информационных исследований по науке, образованию и технологиям ИНИОН РАН совместно с Институтом экономических стратегий проводят МОСКОВСКИЙ ГОРОДСКОЙ СЕМИНАР ПО НАУКОВЕДЕНИЮ И НАУКОМЕТРИИ

С 22 по 28 мая 2019 года в Архангельске проводится ежегодная 21-я Неделя арктической науки (Arctic Science Summit Week), учрежденная Международным арктическим научным комитетом (МАНК/IASC). Тематическая направленность саммита в 2019 году – «Изменения климата и обеспечение жизнедеятельности населения Арктики».

Текущие конкурсы


Российский научный фонд объявляет о начале приема заявок на «молодежные» конкурсы Президентской программы исследовательских проектов. Конкурсы проводятся по всем областям знания, предусмотренным классификатором РНФ, однако, научные исследования должны быть направлены на решение конкретных задач в рамках одного из определенных в Стратегии научно-технологического развития Российской Федерации приоритетов.

Конкурс на лучшие научные проекты междисциплинарных фундаментальных исследований

Конкурс на лучшие проекты организации российских и международных научных мероприятий, проводимых в марте - декабре 2019 года на территории Российской Федерации

Конкурсы 2019 года на лучшие научные проекты фундаментальных исследований, проводимые совместно РФФИ и АНО ЭИСИ

Фонд инфраструктурных и образовательных программ совместно с Агентством по инновациям Израиля (бывший Офис главного ученого Министерства экономики Израиля) проводят восьмой отбор российско-израильских проектов промышленных научно-исследовательских и опытно-конструкторских работ.

Вакансии


08.02.2019
объявляет о проведении выборов на должность заведующего академической кафедрой истории и философии науки.

14.09.2018
ФГБУН Институт геологии рудных месторождений, петрографии, минералогии и геохимии Российской академии наук (ИГЕМ РАН)объявляет конкурс на замещение вакантных должностей

13.04.2018
Федеральное государственное автономное образовательное учреждение высшего образования “Московский физико-технический институт (государственный университет)” объявляет конкурс на замещение должностей педагогических работников, относящихся к профессорско-преподавательскому составу


опрос

Какие рубрики нашей газеты Вам наиболее интересны?




Copyright 2010
Главная страница   |   О газете  |  Партнеры  |  Команда Поиска  |  Вакансии