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