Имхо, математики обязаны принять единый стандарт подачи теорем и их доказательств — только на неком формальном языке, путь там coq или любой другой. Чтобы человеческие ресурсы на проверку не тратились и была однозначность.
Так же это будет первым шагом к тому, что ИИ сам решал мат. проблемы.
Ну и такой вопрос. Что мне делать, если я хочу поработать в этом направлении, но не имею ББД? Или же не возможно это все?
Здравствуйте, Shmj, Вы писали:
S>Интересна ли вам тема формализации математики?
Нет.
S>Так же это будет первым шагом к тому, что ИИ сам решал мат. проблемы.
А как ИИ научить основным понятиям и аксиомам? Вновь же все упрется не в математику, а в лингвистику.
Здравствуйте, pagid_, Вы писали:
_>А как ИИ научить основным понятиям и аксиомам?
Ну собственно системы доказательства теорем по заданным аксиомам раньше и назывались ИИ, до моды на черные ящики нейросетей.
_>Вновь же все упрется не в математику, а в лингвистику.
Ну а как мы учим компьютеры делать то, что требуется? У нас своя, программерская лингвистика и языки программирования.
Здравствуйте, graniar, Вы писали:
G>Ну собственно системы доказательства теорем по заданным аксиомам раньше и назывались ИИ, до моды на черные ящики нейросетей.
И как успехи, близка математика к формализации в терминах Shmj ?
G>Ну а как мы учим компьютеры делать то, что требуется? У нас своя, программерская лингвистика и языки программирования.
Осталось создать математическую лингвистику. Стоп, она уже есть, но задачу решить пока не особо помогла.
Программистская лингвистика и языки программирования основана на компьютерных примитивах. А тут всего-то лишь надо отобразить примитивы математической модели мира на компьютерные. Займитесь.
Здравствуйте, pagid_, Вы писали:
_>И как успехи, близка математика к формализации в терминах Shmj ?
В процессе.
_>Осталось создать математическую лингвистику. Стоп, она уже есть, но задачу решить пока не особо помогла.
Значит требует доработки.
_>Программистская лингвистика и языки программирования основана на компьютерных примитивах. А тут всего-то лишь надо отобразить примитивы математической модели мира на компьютерные. Займитесь.
Здравствуйте, Shmj, Вы писали:
S>Интересна ли вам тема формализации математики?
S>Имхо, математики обязаны принять единый стандарт подачи теорем и их доказательств — только на неком формальном языке, путь там coq или любой другой. Чтобы человеческие ресурсы на проверку не тратились и была однозначность.
Лет 100 уже как есть. Матлогика раздел математики
S>Так же это будет первым шагом к тому, что ИИ сам решал мат. проблемы.
Давно уже решает, но не то чтобы хорошо работало на практике
Здравствуйте, __kot2, Вы писали:
S>>Имхо, математики обязаны принять единый стандарт подачи теорем и их доказательств — только на неком формальном языке, путь там coq или любой другой. Чтобы человеческие ресурсы на проверку не тратились и была однозначность. __>Лет 100 уже как есть. Матлогика раздел математики
Я не о том. Цель — чтобы все мат. доказательства предоставляли на комп. языке и проверялись компом. Т.е. с самой школы учить записи на комп. языке, строго формальном.
А то один математик японский якобы доказал некую теорему, но никто не может понять доказал ли он, т.к. оно все настолько сложное, что никто не может понять — гений он или дурак.
Здравствуйте, Shmj, Вы писали:
S>Я не о том. Цель — чтобы все мат. доказательства предоставляли на комп. языке и проверялись компом. Т.е. с самой школы учить записи на комп. языке, строго формальном.
S>А то один математик японский якобы доказал некую теорему, но никто не может понять доказал ли он, т.к. оно все настолько сложное, что никто не может понять — гений он или дурак.
Так никто и не поймет проверка копом сделана корректно или нет. И так и не узнает гений он или дурак. И нужно ли оно кому-то было.
Здравствуйте, pagid_, Вы писали:
_>Так никто и не поймет проверка копом сделана корректно или нет. И так и не узнает гений он или дурак. И нужно ли оно кому-то было.
Там грубо говоря получится так — если скомпилировалось — то корректно. Или искать ошибку в компиляторе, но там все просто — основано на банальных аксиомах.
Здравствуйте, Shmj, Вы писали:
S>Там грубо говоря получится так — если скомпилировалось — то корректно. Или искать ошибку в компиляторе, но там все просто — основано на банальных аксиомах.
А ошибку в компиляторе найти проще, чем проверить доказательство? И если бы там все было просто, то и доказательство было бы проверить просто.
Надо начать примерно с книг А. Шеня. Трёхтомник там, введение в основания математики. Я на эту тему давно читал. Мало в чём разобрался, не особо стремлясь, но там по-моему проблема в том, что то ли с такой постановкой вопроса с самой проблемы, то ли с невозможностью решить такую задачу в принципе.
Здравствуйте, Shmj, Вы писали:
S> Чтобы человеческие ресурсы на проверку не тратились и была однозначность.
Нет, так не получится. ИИ и формализация — "перпендикулярные" друг к другу сущности. ИИ (то, что под ним сейчас понимают) занимается поиском закономерностей/последовательностей, а формализация — это набор строгих правил. Попытка заставить ИИ проверять формальные правила приведёт к ошибкам. Шахматы — игра со строгими формализованными правилами. Попытка играть в шахматы с ChatGPT ведёт к странным результатам. пример. С другой стороны, математические доказательства почти всегда содержат неформальный элемент и этим отличаются от формального вывода. Самый простой пример неформального элемента это, наверное, доказательство начинающиеся словами "проведём доказательство от противного". Само то, что доказательство надо проводит "от противного" формально никак ниоткуда не следует. И вот такими приёмами доказательства отличаются от простых математических выводов. Причём количество таких приёмов, вроде бы, ничем не ограничено. Так что возможно, что ИИ сможет придумать доказательство, но каждое такое доказательство придётся проверять независимо от ИИ.
Здравствуйте, B0FEE664, Вы писали:
BFE>Самый простой пример неформального элемента это, наверное, доказательство начинающиеся словами "проведём доказательство от противного".
Который тоже прекрасно формализуется. Например:
Если верно A, значит верно как минимум одно из множества {B,C}
Если верно B, значит неверно D
Отсюда следует, что если верны A и D, то верно C
Более конкретный пример — доказательство иррациональности sqrt(2)
Корень либо рационален, либо иррационален. Если он рационален, то он целый, но если он целый, его квадрат не может равняться двум.
Остается единственный вариант, что он иррационален.
Здравствуйте, graniar, Вы писали:
BFE>>Самый простой пример неформального элемента это, наверное, доказательство начинающиеся словами "проведём доказательство от противного". G>Который тоже прекрасно формализуется.
Я не про метод, а про выбор. Почему выбрано "доказательство от противного", а не какой-то другой способ доказательства?
Здравствуйте, B0FEE664, Вы писали:
BFE>Я не про метод, а про выбор. Почему выбрано "доказательство от противного", а не какой-то другой способ доказательства?
Не уверен, что понял вопрос. "Доказательство от противного", этот тот же самый "Метод исключений", просто не указывается явно множество вариантов.
То есть, вся неформальность просто в неуказании некоторых шагов, которые слишком очевидны.
Здравствуйте, graniar, Вы писали:
BFE>>Я не про метод, а про выбор. Почему выбрано "доказательство от противного", а не какой-то другой способ доказательства? G>Не уверен, что понял вопрос. "Доказательство от противного", этот тот же самый "Метод исключений", просто не указывается явно множество вариантов. G>То есть, вся неформальность просто в неуказании некоторых шагов, которые слишком очевидны.
В указании некоторых шагов, которые совершенно не очевидны. Откуда нам знать, что нужно сделать, какой метод применить? "От противного", "по индукции" или ещё какой, специфичный для данного вида задач.
Здравствуйте, B0FEE664, Вы писали:
BFE>В указании некоторых шагов, которые совершенно не очевидны. Откуда нам знать, что нужно сделать, какой метод применить? "От противного", "по индукции" или ещё какой, специфичный для данного вида задач.
Ну это уже будет немного другое. Формализация мышления как такового, а не просто математики, как области знаний.
Здравствуйте, Shmj, Вы писали: S>А то один математик японский якобы доказал некую теорему, но никто не может понять доказал ли он, т.к. оно все настолько сложное, что никто не может понять — гений он или дурак.
Спорим, ты не сможешь привести доказательство на нормальный источник
