Журнал "Компьютерра" №759

Комментируя эту новость, обычно вспоминают о клонировании мамонтов. Конечно, возможность их оживления еще под вопросом. И дело не только в том, что вечная мерзлота хуже японских морозильников. При клонировании ядра пересаживают в яйцеклетки того же вида, а яйцеклеток мамонтов у исследователей как раз и нет. Для этих целей придется использовать яйцеклетки слона как наиболее близкого родственника мамонта из ныне живущих, но вероятность получения полноценного клона в этом случае невелика. И все же значение успеха японских биологов не стоит недооценивать. Даже если сейчас неясно, где могут "выстрелить" такие технологии, расширение границ возможного порой способно приносить плоды в самых неожиданных областях.

А где применять результаты другого исследования, не нужно и гадать. Группа Йосики Сасаи (Yoshiki Sasai), трудящаяся в том же Центре биологии развития, смогла вырастить из отдельных клеток участки мозговой ткани. Ученые использовали как эмбриональные стволовые клетки, так и индуцированные плюрипотентные клетки из тканей взрослого человека. Ясно, что применение второй категории клеток гораздо предпочтительнее. Лучше "омолодить" клетки взрослого человека, нежели использовать материал из абортированных зародышей. Но в обоих случаях, направляя рост и размножение делящихся нервных клеток, ученым удавалось вырастить фрагменты нервной ткани. Нейроны располагались в них закономерным образом, устанавливали контакты друг с другом и даже обменивались сигналами. Хотя метод пока рано использовать в медицинской практике, выращенные фрагменты ткани уже годятся, например, для тестирования лекарств. ДШ

Важные проблемы современного состояния математики поднимает декабрьский выпуск журнала Notices of the American Mathematical Society, центральная тема которого посвящена формальным доказательствам.

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

Но в последние десятилетия и в привилегированной касте математиков появились сомнения. Что такое строгое математическое доказательство в научной статье или книге? Оно написано человеком и для человека. Хуже того, специалистом и для специалиста. И где гарантии, что в нем нет ошибок? Аргументы в статье излагаются в повествовательной форме, облегчающей их восприятие. Многие известные результаты неявно предполагаются, многие вроде бы очевидные специалисту детали опускаются, и зачастую текст опирается на развитую интуицию профессионалов. Корректность аргументов в доказательстве оценивается другими математиками, порою в неформальных дискуссиях. В результате развитие математики превращается в некий социальный процесс в замкнутой среде.

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

Чтобы обойти эти проблемы, программисты и математики еще с пятидесятых годов прошлого века стали развивать область формальных доказательств. Доказательство кодируется на языке формальной логики, а специальная программа проверяет его корректность. И кодировка доказательства, и программа его проверки тоже могут содержать ошибки, но таких программ уже несколько и многократная проверка вселяет уверенность в надежности доказательства. В последние годы программы проверки доказательств стали достаточно мощными, чтобы справляться со сложными теоремами. К сожалению, формальная запись доказательства пока получается примерно в четыре раза длиннее обычной и требует примерно неделю муторной напряженной работы, чтобы формализовать одну страницу. И надо очень любить математику и программирование, чтобы этим заниматься. Тем более что славы проверка известных теорем не приносит. Впрочем, программы совершенствуются, и, возможно, в недалеком будущем запись формального доказательства станет не намного труднее записи обычного. А редакции математических журналов не станут рассматривать статьи без приложения формальных записей сформулированных в них теорем.

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

В конце октября медиахолдинг ВГТРК подал несколько исков, связанных с защитой своих авторских прав. Ответчиками по ним являются крупнейшая российская интернет-компания Mail.ru, а также социальная сеть "Вконтакте". Правда, на сайте Арбитражного суда Москвы пока имеются сведения только о двух исках, поданных к Mail.ru, с датами рассмотрения 24 ноября и 10 декабря.

Причина исков не оригинальна: нарушение авторских прав. Вернее, вопрос о том, кто должен за это отвечать - владельцы сайта, на который можно загрузить охраняемые копирайтом материалы, или его пользователи. По словам главного редактора канала "Вести" Дмитрия Медникова, холдинг намерен судиться со всеми, кто незаконно распространяет их контент. Он заявил, что причиной иска стало то, что наряду с короткими роликами на сайтах ответчиков начали появляться программы, сериалы и фильмы целиком. ВГТРК добивается, чтобы все сайты, на которых появляются видеофайлы с их передачами, начали сотрудничать с владельцами смежных прав.

В принципе, короткие ролики вполне подпадают под нормы ГК о цитировании, поскольку закон никак не регламентирует то, какие произведения могут цитироваться. Однако с произведениями целиком этот номер, разумеется, не проходит.

На Западе в таких случаях применяется принцип "безопасной гавани" (safe harbor): владелец сайта, на который пользователи загружают охраняемый авторским правом контент, может быть освобожден от ответственности, если в его действиях не содержится никакой вины (он не мог знать о нарушении чужих прав и предотвратить их). В отечественном законодательстве нечто подобное закреплено в статье 1064 Гражданского кодекса: чтобы избежать ответственности, лицо, причинившее вред, должно доказать отсутствие своей вины. Однако сделать это в случае с Mail.ru будет проблематично: ведь придется сперва установить личность пользователя, загрузившего ролик на сайт, и привлечь его к суду в качестве надлежащего ответчика.

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

Примерно то же самое может произойти и с ответчиками по искам ВГТРК, причем даже с большей вероятностью: в случае с "Мастерхостом" потенциальным нарушителем было все-таки одно юридическое лицо, а не множество физических.