Критерий истинности в математике

[Rasool]

epros в сообщении #1134473 писал(а):

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

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

[epros]

Rasool в сообщении #1135739 писал(а):

Пока профессиональные математики в основном доказывают теоремы с помощью своей головы, а не с помощью компьютера.

И Вы отсюда делаете вывод, что большинство доказанного математиками компьютер доказать не может? Вовсе нет.

[Anton_Peplov]

Здесь важно не смешивать разные смыслы выражения "компьютер может доказать".

Первый вопрос - можно ли данное математиками неформальное доказательство перевести на язык какой-то "стандартной" формальной теории. Я не в курсе, честно говоря, в чем они там доказывают - в формальной ZFC или еще где-то, но факт в том, что теория не выдумывается специально под эту конкретную теорему - так можно было бы включить ее в список аксиом и дело с концом - а берется стандартная теория со стандартными аксиомами, и на ее языке записывается доказательство. Обычно считается, что на формальный язык можно перевести любое доказательство, хотя Вавилов, например, сомневается, что это можно сделать с топологическими доказательствами, использующими картинки. После того, как формальное доказательство построено, компьютер может проверить его и в этом смысле "доказать" теорему. Другой вопрос, сколько времени у человека займет перевод с неформального языка на формальный. Это очень трудоемкий процесс, и есть даже мнение, что для серьезных теорем практически неподъемный.

Второй вопрос - а может ли компьютер не проверить составленное человеком формальное доказательство, а самостоятельно его найти за разумное время? Здесь пока все плохо, к сожалению. Т.е. алгоритмически никаких проблем - перебираем все доказательства, пока одно из них не окажется доказательством нужного утверждения или противоположного (как завещал вождь и учитель Гедель, на каких-то утверждениях мы зациклимся, но на самом деле таких утверждений еще поискать; их можно конструировать специально, но чтобы интересное нам утверждение по закону подлости оказалось недоказуемым - это вряд ли). Идиллию портит оговорка "за разумное время", потому что ждать $100^{500}$ лет - удовольствие ниже среднего.

[epros]

Anton_Peplov в сообщении #1135744 писал(а):

Второй вопрос - а может ли компьютер не проверить составленное человеком формальное доказательство, а самостоятельно его найти за разумное время? Здесь пока все плохо, к сожалению.

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

[Anton_Peplov]

Нет, я говорю вот о чем. Пусть мы точно знаем, что нам нужно доказательство ВТФ. Записываем ВТФ на языке формальной теории. Вопрос: как компьютеру найти доказательство этого утверждения? Сферический алгоритм в вакууме существует: перебирать все конечные строки языка теории, отделять доказательства и проверять, является ли найденное доказательство доказательством ВТФ. Надежды, что этот алгоритм остановится раньше, чем погаснет Солнце, нет совсем никакой.

[whitefox]

Anton_Peplov в сообщении #1135862 писал(а):

Записываем ВТФ на языке формальной теории. Вопрос: как компьютеру найти доказательство этого утверждения?

Метод резолюций. Хотя это и не сферический метод в вакууме, но фактически эквивалентен решению SAT-проблемы.

Подробности тут: Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем.

[mihaild]

Anton_Peplov в сообщении #1135744 писал(а):

время? Здесь пока все плохо, к сожалению

Уже для евклидовой геометрии всегда будет всё плохо - задача истинности формул в ней EXPTIME-трудна. Можно только пытаться рассматривать эвристики разного качества.

[epros]

Хочу сказать всем защитникам преимуществ человеческого разума перед бездушными машинами: Экспоненциальная сложность задачи поиска доказательства для человека такая же непреодолимая проблема, как и для компьютера. И никакая математическая интуиция или другие формы оракулов тут не помогут. Другое дело, что человек вполне может что-нибудь добавить в аксиоматику, если сочтёт это полезным для облегчения доказательства. Компьютер такого делать не станет (если явно ему этого не разрешить).

[mihaild]

epros, разве доказано, что $BQP \neq EXPTIME$?

[epros]

mihaild в сообщении #1135946 писал(а):

epros, разве доказано, что $BQP \neq EXPTIME$?

Я не понял, это намёк на то, что в мозгах математиков - квантовый компьютер? Давайте тогда наймём кого-нибудь из них в криптоаналитики, чтобы с помощью алгоритма Шора за время $N^3$ в уме шифры взламывали.

[Anton_Peplov]

epros в сообщении #1135940 писал(а):

Экспоненциальная сложность задачи поиска доказательства для человека такая же непреодолимая проблема, как и для компьютера.

Ну Уайлс же не доказывал ВТФ полным перебором строк, похожих на доказательство, нес па? Или он в аксиоматику что-то добавил?:) "А примем-ка мы за аксиому, что ВТФ верна".

У некоторых людей, эта, крутые эвристики есть. Ну очень крутые. Мы плохо пока понимаем, какие именно - если бы понимали и научились воспроизводить, у нас каждый выпускник математического факультета был бы Уайлсом. Так вот именно потому, что мы не понимаем, что это за эвристики, мы не можем их запрограммировать, чтобы они были у компьютера. И пока это так, компьютер в деле поиска математических доказательств, быть может, и не будет проигрывать бухгалтеру тете Маше, но Эндрю Уайлсу точно будет проигрывать.

[Rasool]

Anton_Peplov в сообщении #1135955 писал(а):

epros в сообщении #1135940 писал(а):

Экспоненциальная сложность задачи поиска доказательства для человека такая же непреодолимая проблема, как и для компьютера.

Ну Уайлс же не доказывал ВТФ полным перебором строк, похожих на доказательство, нес па? Или он в аксиоматику что-то добавил?:) "А примем-ка мы за аксиому, что ВТФ верна".

У некоторых людей, эта, крутые эвристики есть. Ну очень крутые. Мы плохо пока понимаем, какие именно - если бы понимали и научились воспроизводить, у нас каждый выпускник математического факультета был бы Уайлсом. Так вот именно потому, что мы не понимаем, что это за эвристики, мы не можем их запрограммировать, чтобы они были у компьютера. И пока это так, компьютер в деле поиска математических доказательств, быть может, и не будет проигрывать бухгалтеру тете Маше, но Эндрю Уайлсу точно будет проигрывать.

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

[mihaild]

epros в сообщении #1135953 писал(а):

Я не понял, это намёк на то, что в мозгах математиков - квантовый компьютер?

Это намек на то, что мы не можем уверенно утверждать, что классический компьютер не уступает мозгу (при стремлении размеров компьютера и мозга к бесконечности:D).

[Anton_Peplov]

Rasool в сообщении #1135963 писал(а):

В принципе, математик должен сам разрабатывать такие эвристики.

К сожалению, эти эвристики сидят где-то у него в подсознании. Выковырять их оттуда и показать он не может. Он может предъявить доказательство, но не путь, которым пришел к доказательству, потому что важные компоненты этого пути скрыты от него самого. Ну скажет он "я думал о том-то, потом по аналогии о том-то, и неожиданно понял, что..." Что скрыто за этим "неожиданно", и есть загадка. Инсайт (как и творчество в целом) - большая тайна, в том числе для самого творца.

[epros]

Anton_Peplov в сообщении #1135955 писал(а):

Или он в аксиоматику что-то добавил?:)

А разве нет? Вроде, он доказал её отнюдь не в аксиоматике Пеано первого порядка. То бишь, аксиоматика явно была сильнее, чем минимально необходимая.

Anton_Peplov в сообщении #1135955 писал(а):

"А примем-ка мы за аксиому, что ВТФ верна"

Ну, это вряд ли было бы интересно коллегам. А вот если постулировать какое-нибудь существование какого-нибудь недостижимого кардинального числа или что-то в этом роде, так, глядишь, и станет интересным.

Anton_Peplov в сообщении #1135955 писал(а):

У некоторых людей, эта, крутые эвристики есть. Ну очень крутые. Мы плохо пока понимаем, какие именно

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

Anton_Peplov в сообщении #1135955 писал(а):

Так вот именно потому, что мы не понимаем, что это за эвристики, мы не можем их запрограммировать, чтобы они были у компьютера

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

mihaild в сообщении #1135965 писал(а):

не можем уверенно утверждать, что классический компьютер не уступает мозгу

Я бы сказал, что у нас нет никаких оснований утверждать, что компьютер уступает мозгу при эквивалентной производительности и правильных базовых алгоритмах.