Официально


Кабинету министров вместе с Президиумом Совета при Президенте РФ по науке и образованию поручено к концу ноября разработать и утвердить меры по созданию и эксплуатации уникальной научной установки класса мегасайенс на острове Русский.



Заместителем министра просвещения РФ назначен Андрей Николаев. Распоряжение об этом подписал премьер Дмитрий Медведев.

Рособрнадзор запретил прием в Вятский государственный университет. Санкция применена за «неисполнение предписания в установленный срок».

Два опорных селекционно-семеноводческих центра в области сахарной свеклы будут созданы на базе ВНИИ сахарной свеклы и сахара им. А.Л.Мазлумова (Воронежская область) и Первомайской селекционно-опытной станции сахарной свеклы (Краснодарский край). Такое решение одобрил Межведомственный совет при Министерстве науки и высшего образования по вопросам, связанным с реализацией подпрограммы «Развитие селекции и семеноводства сахарной свеклы в РФ».




Новости № 41(2018)

Регионы


Первый МГМУ им. И.М.Сеченова открыл новое направление подготовки - “Промышленная фармация”. Вуз предложил учащимся два уникальных профиля этой магистерской программы - “Обеспечение качества лекарственных средств” и “Управление разработкой лекарственных средств”.

Ярославский госуниверситет подписал трехстороннее соглашение с ярославским филиалом Физико-технологического института РАН и “Ростовским оптико-механическим заводом”.

Губернатор Ставропольского края Владимир Владимиров ознакомился с ходом строительства нового учебно-лабораторного корпуса Аграрного университета.

СНГ


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


Телескоп “Хаббл” обнаружил объект размером с Нептун - потенциальный спутник далекой планеты. С подробностями - Sciencemag.org.

В конце сентября экспертный совет при Министерстве здравоохранения и науки Японии представил рекомендации относительно использования инструментов генного редактирования в эмбрионах человека.

Спутниковые лазерно-радарные исследования выявили ранее недооценные размеры и сложную устроенность поселений древней цивилизации майя в период ее расцвета и даже раньше.


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
















Виден выход из норы. Труд математиков можно облегчить.
Наука
№ 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 мог бы очень помочь, потому что он освобождает мозг от бесконечных проверок и перепроверок самого себя - не столько даже от рутины, сколько от неуверенности.
- Как вам видится - наверное, ваш проект бесконечный, его завершить нельзя? Как стремление к совершенству.
- Его не то чтобы нельзя завершить. Я хотел бы создать нечто, что будет жить. То есть придать этому информационному, интеллектуальному существу какие-то начальные правила и параметры, которые позволят ему развиваться дальше. И именно поэтому я вкладываю огромную энергию в то, чтобы у него была крепкая основа, чтобы оно могло долго расти и приносить пользу.

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


 

Отзывы

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



 

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

Гибель во спасение. Опухолевые клетки доведут до самоубийства.
Борис Давидович Животовский - ведущий специалист в области исследования программируемой гибели клеток. Одно из наиболее перспективных мировых направлений в биомедицине ведет к разработке эффективных подходов к лечению многих заболеваний. /№ 41(2018)
Стой, кто идет? Клетки учат противостоять болезням.
С директором Института биоорганической химии им. академиков М.М.Шемякина и Ю.А.Овчинникова РАН (ИБХ РАН) академиком Александром ГАБИБОВЫМ мы собирались побеседовать о новых исследованиях, проводимых в возглавляемой им лаборатории биокатализа. Прежде всего, по гранту, поддержанному в рамках Президентской программы РНФ, “Структурные и кинетические особенности презентации антигенов как ключ к пониманию механизмов индукции аутоиммунных патологий и лимфомогенезиса”. /№ 40(2018)
Иногда они просыпаются. Вулканы Камчатки дают массу ценной информации ученым.
Сотрудники Института нефтегазовой геологии и геофизики им. А.А.Трофимука СО РАН (Новосибирск) держат под особым контролем активные вулканы Камчатки, ведь извержения в этом регионе могут представлять опасность для тихоокеанских воздушных трасс и Петропавловска-Камчатского. /№ 40(2018)

Новости


Около 100 делегатов из разных регионов России стали участниками IX Всероссийского съезда советов молодых ученых в Сочи. Мероприятие проходило в рамках саммита молодых ученых и инженеров «Большие вызовы для общества, государства и науки», для участия в котором были отобраны более 250 студентов из 78 университетов более чем 20 регионов России.



Состоялся IV Форум ректоров университетов Российской Федерации и Республики Куба.



Почти треть российских вузов, обращавшихся за получением государственной аккредитации в 2018 году, воспользовалась электронной формой подачи документов, сообщает пресс-служба Рособрнадзора.



В преддверии 60-летия Государственной публичной научно-технической библиотеки России ее генеральный директор Яков Шрайберг рассказал о том, как будет развиваться ГПНТБ в ближайшем будущем. Текст его выступления размещен на сайте библиотеки.

Томские вузы планируют создать «Сибирский научно-образовательный центр (НОЦ) новой технологической революции», объединившись с промышленными партнерами. Об этом рассказал ТАСС в кулуарах форума U-NOVUS ректор Томского государственного университета Эдуард Галажинский.

Сотни тысяч человек стали гостями и участниками фестиваля NAUKA 0+, тема которого в этом году звучала так: «Мегасайенс: Россия в мире - Россия для мира».

Дистанционные образовательные курсы нужны, но они никогда не заменят очных лекций, заявил ректор МГУ им. М.В.Ломоносова Виктор Садовничий на III Форуме ректоров иберо-американских и российских университетов.

Конференции


С 3-го по 7 сентября 2018 года на базе ФГБНУ “Северо-Кавказский федеральный научный центр садоводства, виноградарства, виноделия” под патронажем Министерства науки и высшего образования РФ, Российской академии наук будет проводиться Международный научно-практический форум “Перспективные технологии и сортименты в садоводстве, виноградарстве, виноделии”

XIV Андриановская конференция прошла в июне в ИНЭОС РАН

II Всероссийская научно-практическая конференция “Совершенствование системы взаимодействия Российского фонда фундаментальных исследований и субъектов Российской Федерации в вопросах проведения региональных и молодежных конкурсов”

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


“Сколково” и “Химпром” продолжают искать проекты малотоннажной химии

До 29 октября 2018 года идёт прием заявок на участие в конкурсе на соискание премий Правительства Москвы молодым ученым, присуждаемых ежегодно с 2013 года.

Конкурс на лучшие научные проекты фундаментальных исследований, проводимый совместно федеральным государственным бюджетным учреждением “Российский фонд фундаментальных исследований” и Фондом “Дом наук о человеке” Франции

Конкурс на лучшие научные проекты фундаментальных исследований, проводимый совместно федеральным государственным бюджетным учреждением “Российский фонд фундаментальных исследований” и Вьетнамской академией общественных наук

Конкурс на лучшие научные проекты фундаментальных исследований, проводимый совместно федеральным государственным бюджетным учреждением “Российский фонд фундаментальных исследований” и Министерством образования и науки Республики Южная Осетия

Вакансии


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

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

02.03.2018
объявляет конкурс на замещение вакантных должностей:




опрос

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




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