Вычисляемые знания и будущее чистой математики

[Valery35]

Спасибо. А то «серьезные» приложения на хабре последнее время уступают место сиюминутным вопросам.

[vxsw]

99,(9)% дистиллят матана на хабре, респект!

[dimakovalenko]

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

Прикольно. Только вот сколько среди этих 5 миллионов утверждений — ошибочных утверждений? Даже дотошные товарищи вроде Уайта — и то ошибались в самых что ни на есть серьезных работах. Ведь первая попытка вроде бы безупречного со всех сторон доказательства теоремы Ферма провалилась чисто случайно — в нем нашли ошибку только «коллективным разумом» присутствующих на докладе математиков, причем математиков незаурядных. А был бы доклад или статья на какую-то будничную тему, ее бы увидел всего один рецензент и не факт что нашел бы там ошибку.

[OsipovRoman]

Поэтому Стивен и пишет:

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

[dimakovalenko]

Я не вполне ясно выразил свою мысль, извините. Мне просто «мобилизация математиков» не кажется хорошей идеей (сколько ошибок они пропустят и сколько своих наделают?) Потому что даже звезды вроде Уайта ошибаются. По-моему стоило предложить какую-то автоматическую систему проверки теорем отталкиваясь от основных аксиом, как Вы считаете?

[OsipovRoman]

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

[dimakovalenko]

Согласен, да :)
Спасибо за статью!

[tower120]

А этот «step-by-step solution» в самом Wolfram Mathematica есть?
Если да, то куда клацать? :)

[OsipovRoman]

Есть через интеграцию с Wolfram|Alpha, подробнее.

[tower120]

Так оно кажется онлайн. Ну, в смысле, все запросы на сервер посылает, и там обрабатывает.
Или я путаю?

[OsipovRoman]

Да, запрос вы отправляете на Wolfram|Alpha и без интернета это работать не будет.

[tower120]

Эхх… А казалось бы…
Solve есть? Есть. Что мешало бы показать по шагово?
И вообще Wolfram|Alpha чет нарядней самой Mathematica.

[OsipovRoman]

Я думаю, зная концепию компании, что в ближайшее время скорее всего в Wolfram Language появится функция вроде StepByStepSolutio, которая будет напрямую выдавать пошаговые решения. Сейчас же вы можете легко обратиться через функцию WolframAlpha к пошаговым решениям и выцепить его, создать свой интерфейс.

Вот пример для, скажем, пошагового метода Гаусса:

DynamicModule[{i, j, tF, res, resLength, x}, 
 Panel[Grid[{{Row[{Style["Количество строк:          ", 
        FontFamily -> "Myriad Pro Cond", 30], 
       InputField[Dynamic[i], Number, 
        FieldSize -> {5, 1}]}]}, {Row[{Style["Количество столбцов: ", 
        FontFamily -> "Myriad Pro Cond", 30], 
       InputField[Dynamic[j], Number, 
        FieldSize -> {5, 1}]}]}, {}, {Style["Матрица: ", 
      FontFamily -> "Myriad Pro Cond", 30]}, {Dynamic@
      Grid[Table[
        With[{iD = iI, jD = jI}, 
         InputField[Dynamic[x[iD, jD]], Number, 
          FieldSize -> {2, 1}]], {iI, 1, i}, {jI, 1, j}], 
       Dividers -> {True, True}]}, {}, {Row[{Style[
        "Произвести расчет:    ", FontFamily -> "Myriad Pro Cond", 
        30], Checkbox[Dynamic[tF]]}]}, {Dynamic[
      If[tF, res = 
        WolframAlpha[
          "row reduce " <> 
           ToString@
            Table[x[ii, jj], {ii, 1, i}, {jj, 1, j}], {{"Result", 2}, 
           "Content"}, 
          PodStates -> {"Result__Step-by-step solution"}][[1, 1, 1, 1,
          1]]; resLength = Length[res]; 
       Manipulate[
        Style[Grid[{{Pane[
             Row[{"Шаг ", step, " из ", resLength}], {600, 30}, 
             Alignment -> Center]}, {Pane[
             DisplayForm[
              res[[step, 1, 1, 1, 1, 1]] /. 
               GrayLevel[0.5`] -> Black], {600, 50}, 
             Alignment -> Center]}, {Pane[
             DisplayForm[res[[step, 1, 1, 1, 2, 1]]], {600, 300}, 
             ImageSizeAction -> "ResizeToFit", 
             Alignment -> Center]}}], 
         FontFamily -> "Myriad Pro Cond"], {{step, 1, "Шаги"}, 1, 
         Length[res], 1}], 
       Style["", FontFamily -> "Myriad Pro Cond"]]]}}, 
   Alignment -> Left, ItemStyle -> {Bold, 18}]],
 Initialization :> {i = 4; j = 5; tF = False; 
   Table[x[ii, jj] = RandomInteger[{-5, 5}], {ii, 1, i}, {jj, 1, j}]}]

На вы ходе вы получите:



Что же касается нарядности, то Mathematica нет нужды по умолчанию выглядеть сильно нарядно, если это необходимо (скажем, сделать электронный учебник, презентацию, пользовательский интерфейс), то сделать его нарядным не составит труда. Кстати картинка в начале — это просто код на языке Wolfram Language.

[tower120]

Эхх встраивали CDF player, встравивали. А в результате опять картинками кидаются :))

[OsipovRoman]

Я не уверен, что Хабр даст встроить интерактивный контент, так что дело не в CDF.

[tower120]

А ссылкой нельзя?

[ankh1989]

За что минусуют этот коммент? Ведь интеллект этим и занимается: берёт всякие разные факты и пытается придумать что нибудь полезное основываясь на этих фактах. Доказательство теорем — наиболее чистая форма этого процесса. Мистер Вольфрам хочет как раз это и сделать. Идея, прямо скажем, не нова, но и Вольфрам — человек незаурядный и может что нибудь и придумает.

[OsipovRoman]

С тем, что Стивен делает сенсацию из ничего не согласен, если вы читали его труд «A New Kind of Science», то вы поймете почему он взорвал научное сообщество на западе 10 лет назад. Благодаря ему клеточные автоматы и машины Тьюринга получили огромную популярность и широкое практическое применение. Они были известны и до него, но красоту в них мы увидели пожалуй благодаря Стивену. А что касается, скажем, «нового языка математики» и «big math» — это просто то, чем уже нужно заниматься и выделять на это не 100, а и 500 млн. $, просто беда современного мира в том, что на какие-то «фитюльки» вроде игр люди гораздо охотнее готовы потратить хоть миллиард долларов, чем на реально серьезную вещь. Даже если не будет на выходе такой системы, сделать качественную вычисляемую базу по всей чистой математике, обновляемую и дальше — это даст математикам огромную выгоду.

[OsipovRoman]

Скажите, вы читали книгу? Только честно.
Вы можете посмотреть список литературы, которую использовал Стивен при создании своей монографии здесь. Думаю тезис о том, что «не используются достижения в соответсвующих областях науки» отпадает сам собой.
То что вселенная — простейший автомат — на самом деле идея, проистекающая из того, что простые правила создают крайне сложные конструкции в процессе своей эволюции. Если выдирать из контекста, конечно это звучит не очень.

[lightcaster]

Один математик доказал полноту по Тьюрингу правила 110, по конкурсу от Вольфрама. Опубликовал результат, как это принято. Стивен его засудил, и заблокировал публикацию на два года. Это, по вашему, нормально?

[OsipovRoman]

Насколько мне известно, конкурс был один и его победитель получил свой приз.
Сказки какие-то рассказываете.

[lightcaster]

Wikipedia — Rule 110

Around 2000, Matthew Cook published a proof that Rule 110 is Turing complete, i.e., capable of universal computation, which Stephen Wolfram had conjectured in 1985. Cook presented his proof at the Santa Fe Institute conference CA98 before the publishing of Wolfram's book, A New Kind of Science. This resulted in a legal affair based on a non-disclosure agreement with Wolfram Research. Wolfram Research blocked publication of Cook's proof for 2 years.[1]

[OsipovRoman]

Какая-то история высосанная из пальца, чтобы просто очернить Стивена.

Вы разберитесь вначале, а потом говорите.

История простая: Кук был ассистентом Стивена в работе над его книгой и результаты его работы были под соглашением NDA о неразглашении, поэтому до публикации книги ему не дали их опубликовать, что естественно.

[lightcaster]

Да, вы правы. Я напутал. Слил две истории вместе.

Но суть от этого не меняется. Кук доказал правило 110. Стивен через суд заблокировал публикацию.
Да, там был NDA. Но не публиковать важные работы — это странно. Ученый то должен понимать, тем более математик. Вольфрам же подал в суд на собственного работника, чтобы задержать публикацию и перенести ее в свою книгу.

[OsipovRoman]

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

[lightcaster]

Да, я бы сделал иначе. Гугл, фейсбук разрешает публиковаться своим ученым. Более того, это норма. Если мне потребуется, несмотря на DNA я тоже могу договорится с боссом о публикации. Тем более, работа Кука не ноу-хау для бизнеса. Это — теоретический результат.

[OsipovRoman]

Это уже зависит от человека. Я знаю многих «боссов», с которыми договориться не удастся. Все зависит от ценности результатов. Я думаю что никто кроме Стивена и Кука не может рассказать насколько этот «конфликт» был серьезен. С юр. точки зрения все корректно.

[xvilka]

Вот-вот. Univalent Foundations выглядят куда более обнадеживающими.

[Meklon]

Стивен просто демон какой-то. Мне в Альфе не хватает большего контроля над исследованием объекта. Принудительно отобрать синтаксис это не совсем правильно. Хотелось бы гибрида с Mathematica, чтобы была возможность не углубляться в синтаксис, но была возможность задать более конкретно то, что хочу.

[OsipovRoman]

Вы можете использовать Mathematica или интеграцию Wolfram|Alpha c Mathematica. Есть слухи, что в Pro версии это будет через некоторое время. Беда здесь в том, что код Mathematica может содержать что-угодно, поэтому нужна система отсеивания вредоносных программ и еще некоторые вещи. В любом случае, конечно, полную настройку под себя можно делать в Mathematica или Wolfram Cloud, мы вроде бы с вами это уже один раз обсуждали.

[Meklon]

Обсуждали, да. Софт великолепный. Я просто с позиции новичка нематематика рассматриваю. Грубо говоря, Wolfram|Alpha иногда непросто объяснить, чего конкретно ты хочешь, а Mathematica — весьма сложный продукт. Учу понемногу. В целом в восторге от этого комплекса. Но мне, как врачу сильно непросто.

[Indexator]

Получается Wolfram Alpha это такой Google для математиков?..

[OsipovRoman]

Не только, областей которые покрывает Wolfram|Alpha много и их количество растет.

[vilgeforce]

Ух! Можете этой зверюге дать числа 29899 25851 10870 12370 4742 27783 2268 28741? Интересно, найдет ли закономерность. Если найдет — за какое время.

[OsipovRoman]

Если вы имеете ввиду последовательность {29899, 25851, 10870, 12370, 4742, 27783, 2268, 28741} то нет. Если есть закономерность, то такого количества членов мало.

[vilgeforce]

Жаль, что не нашлось. На самом деле даже последних трех чисел хватает для однозначной идентификации алгоритма. Спасибо за информацию!

[OsipovRoman]

Что за алгоритм то?

[vilgeforce]

Последовательные результаты из rand() MSVCRTшного.

[OsipovRoman]

Не думаю что найдется софт, который вам найдет закономерность в псевдослучайных или случайных числах)

[vilgeforce]

На самом деле софт трудится уже три месяца как и дней 10 назад первый практический результат был получен ;-) Но я «в лоб» задачу решал, математика в этой области для меня — темный лес и очень интересно посмотреть на правильное решение задачи.

[The_Electronic_Cat]

Помимо возможных ошибок в «наследии», стоит ожидать и ошибок в работе алгоритмов самого проекта. Представляете эту переписку с саппортом?

«Я много лет с удовольствием пользуюсь вашей разработкой. Благодаря ей я за 11 лет решил проблему Гольдьбаха и подбирался к доказательству гипотезы Римана, когда с разочарованием обнаружил, что доказательство „анонимной теоремы 1728“, сгенерированной программой, содержало пропущенную мною досадную ошибку».
Шелдон Купер

«Вашей заявке присвоен номер №1424987. Она принята на рассмотрение, и наши специалисты свяжутся с вами в кратчайшие сроки. Пожалуйста, не меняйте тему переписки при ответе на это сообщение».