Стив Вольфрам:Вычисляемые знания и будущее чистой математики

[_Ivana]

Вроде еще в середине августа появилась запись в блоге Стивена Вольфрама , через месяц - перевод на Хабре . Я некоторое время назад перестал активно посещать этот форум, может тут и было обсуждение а я не заметил, а может и не особенно интересной показалась сообществу эта запись, во всяком случае, поиском по форуму не нашел. Однако, мне кажется эта публикация и высказанные в ней идеи достаточно интересными, несмотря на то, что я совсем не математик. Но как-то немного грустно становится от осознания того факта, что я вот экспериментально обнаружил и теоретически доказал одну теоремку (насколько я понимаю, ранее не доказанную, может по причине "неуловимого Джо", хотя я на основе нее оптимизировал известный "оптимальный алгоритм"), а послезавтра Стивен научит компьютер выдавать такие теоремки и даже целые абстрактные теории на гора в изобилии, а я как секретарша в конце прошлого века тупо руками перепечатывал на машинке листы или как инженер тупо считал на калькуляторе/логарифмической линейке, а сейчас компьютер сделает то же самое и быстрее и лучше. Что думаете, профессионалы?

ЗЫ может тема не соответствует разделу, пусть тогда модераторы решат где ей лучше быть.

[warlock66613]

Я не профессионал, и мнение профессионалов мне услышать тоже было бы весьма интересно. Но всё-таки я немного пользуюсь вольфрам-продуктами. Так вот, ничего волшебного в них нет: они работают ровно до того момента как ты понимаешь, что делаешь. Как только перестаёшь понимать - они перестают работать. Mathematica без помощи человека не способна решить не только уравнение Шрёдингера (см. соотв. тему на этоим форуме), но даже классическую задачу двух тел. Я пробовал забивать в Mathematica задания из ЕГЭ. Ну, часть B она решила всю, и кое-что из C. Но сложную систему неравенств из C - "не взяла". В общем, по-моему все подобные заявления Вольфрама - чистый маркетинг.

[Pphantom]

Возможно, это немного отвлеченные рассуждения, но, как мне кажется, ситуации похожи...

Лет 15-20 назад в астрономии возникла идея т.н. "виртуальных обсерваторий". Развитие компьютерных сетей и методов работы с базами данных привело к тому, что значительная часть материалов астрономических наблюдений стала появляться сразу в оцифрованном виде и выкладываться в сеть с более или менее общим доступом. Начавшийся примерно тогда же бурный рост числа автоматических и полуавтоматических телескопов привел еще и к быстрому увеличению объема таких материалов. В результате скорость "человеческой" обработки данных стала заметно отставать от темпов их получения, и довольно быстро стали появляться предложения складывать получаемые данные в некотором стандартном формате в определенную базу, из которой всякий желающий мог бы достать то, что ему нужно, и обработать, сэкономив тем самым на непосредственных наблюдениях.

Когда это было реализовано (а это произошло довольно быстро), сразу же возникла идея-продолжение: если есть много стандартизированных данных, то, наверное, можно попытаться автоматизировать и их обработку, извлекая из имеющегося банка данных что-то интересное автоматически. С другой стороны, в те же годы стали популярны идеи Data Mining, так что на это направление буквально набросились, на реализацию этой идеи было потрачено много усилий.

Сейчас, когда прошло уже более десяти лет, можно сказать, что кончилось все это (пока?) ничем или почти ничем. Единичные полученные результаты явно не стоят затраченных на их получение усилий. При этом важно иметь в виду, что астрономия - самая "ботаническая" среди физико-математических наук: только в ней в значительных количествах встречаются задачи сбора данных о большом числе объектов, их классификации и т.д., так что именно тут, казалось бы, для методов DM наибольшее раздолье. Однако оказалось, что даже тут на "человеческое" получение содержательных результатов уходит куда меньше сил, чем на отбор крупиц полезного из вороха результатов автоматической деятельности.

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

[Brukvalub]

Зато вот этот пассаж из статьи Вольфрама: "Миллионы раз в день студенты и другие пользователи вычисляют вещи, такие как интегралы и делают другие расчёты с помощью Wolfram|Alpha, а затем просят эту систему предоставить им пошаговое решение." доказывает, что зато создаваемая им программа уже ежедневно наносит РЕАЛЬНЫЙ ВРЕД созданной за века человечеством системе математического образования.

[nnosipov]

Вред как-то слишком категорично звучит. Это может быть хорошим подспорьем даже в образовании. Пошаговое решение задач надо спрашивать со студентов, не давая им при этом списывать. Т.е. забраковывать решения, полученные "автоматически" с помощью CAS.

[Xaositect]

_Ivana в сообщении #919085 писал(а):

Но как-то немного грустно становится от осознания того факта, что я вот экспериментально обнаружил и теоретически доказал одну теоремку
(насколько я понимаю, ранее не доказанную, может по причине "неуловимого Джо", хотя я на основе нее оптимизировал известный "оптимальный алгоритм"), а послезавтра Стивен научит компьютер выдавать такие теоремки и даже целые абстрактные теории на гора в изобилии, а я как секретарша в конце прошлого века тупо руками перепечатывал на машинке листы или как инженер тупо считал на калькуляторе/логарифмической линейке, а сейчас компьютер сделает то же самое и быстрее и лучше. Что думаете, профессионалы?

Все это давно существует и не работает, по нескольким причинам.
Основная объективная причина - вычислительная сложность поиска доказательства (современная математика на несколько порядков сложнее того примера с булевой алгеброй о которой говорит Вольфрам. Программы, которые выводят или опровергают теоремы этого уровня, давно есть, напр. Prover9). Впрочем, Вольфрам известен тем, что игнорирует чужие исследования в области сложности.
Основная философская причина - это неформализованность понятия "интересного результата" (опять же, пример Вольфрама единичен и слишком прост - он не показывает, например, как выделять новые полезные понятия, что является вещью очень важной)
Программы, которые помогают писать и проверять формальные доказательства, уже тоже давно есть, но они не избавляют математика от работы.

[Brukvalub]

Кстати, подобный "автоматический решатель математических задач" много лет разрабатывает на мех-мате А.С. Подколзин. Коллеги рассказывали мне, что некоторое время назад его программа уже успешно "решала" любую задачу с параметром из раздела С5 ЕГЭ.

[g______d]

Про интегралы, взятые с помощью Mathematica: если она выдает ответ, то шаги интегрирования необязательны. Можно продифференцировать ответ, а потом записать в обратном порядке (интегрируя по частям каждый раз, когда дифференцируется произведение, и меняя переменную, когда дифференцируется композиция).

Общее правило про компьютерные системы -- они хороши (с оговорками), когда делается что-то, для чего есть алгоритм. В частности, задачи с параметрами из ЕГЭ, скорее всего, покрываются теоремой Тарского-Зайденберга, хотя подозреваю, что со временем работы соответствующего алгоритма все печально.

Если класс задач, решаемых с помощью компьютера, расширится, то математика немного поменяется, но не сильно, и в программирование не превратится.

[Munin]

Brukvalub в сообщении #919294 писал(а):

Кстати, подобный "автоматический решатель математических задач" много лет разрабатывает на мех-мате А.С. Подколзин.
Коллеги рассказывали мне, что некоторое время назад его программа уже успешно "решала" любую задачу с параметром из раздела С5 ЕГЭ.

Осталось разработать соответствующий "составлятель математических задач", и ЕГЭ будет полностью автоматизирован!

[kp9r4d]

Munin в сообщении #919373 писал(а):

Осталось разработать соответствующий "составлятель математических задач", и ЕГЭ будет полностью автоматизирован!

Судя по заданиям на ЕГЭ он уже давно разработан.