Существует ли алгоритм для доказательства математических уравнений (теорем,тождеств и пр.)?

У Пойа есть ряд замечательных книг вокруг этих тем "Как решать задачу", "Математическое открытие", "Математика и правдоподобные рассуждения".

Своим студентам я советовал придерживаться такого алгоритма: 1) нарисовать большую разборчивую картинку, 2) спросить себя "как возможно то, что спрашивается", 3) спросить себя "существует ли хоть какая-то связь между тем, что дано и что спрашивается". Опыт показывает, что в значительной доле случаев если задача не решается, то какой-то пункт из этого алгоритма не был выполнен.

Разумеется, всех задач так не решить, но это может быть очень хорошим подспорьем для начала.

Нет.

Да, с некоторыми ограничениями. Если есть логическая цепочка, ведущая к доказательству без озарений вроде "представить 5 в виде суммы 2 и 3, после чего все упрощается". То есть если решение представляется неизвестной цепочкой известных действий. Такой алгоритм реализован в языке программирования Prolog. Собственно, Prolog и является его реализацией с добавлением средств ввода-вывода, выполнения арифметических операций и т. п.

Доказательство теорем - это в некотором смысле творчество, интуиция, а уже потом - логика.
Конкретных алгоритмов не существует, как не существует и правил сочинения музыки, например, или написания картин.
(К примеру, у теоремы Пифагора существует 367 различных доказательств).
Только рекомендация - опираться на установленные (уже доказанные) положения.

Для некоторых классов теорем можно предложить алгоритм доказательства, как систему правил вывода в формальном языке. А в обшем случае - нет. Упирантся это в в "метатеоремы". Математика постоянно "надстраивается",В любой теории появляются теоремы невыводимые в данной теории, относящиеся к более высокому уровню абстракции (метатеоремы) и просто не выводимые (на \том же уровне абстракции) . И, вероятно, процесс этот бесконечен. Исследует этот процесс математическая логика, которую мало кто осваивает дальше алгебры высказываний и теории предикатов. Как математическая проблема - это алгебра (группы, полугруппы, формальные языки, контекстно-свободные языки и более сложные конструкции)

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

То, что можно алгоритмизировать - можно автоматизировать :) В данном случае номер не прокатит...

а я смею утверждать, что ЕСТЬ!!!. вопрос, как всегда, поставлен чуть некорректно - вообще!... есть совершенно различные так сказать "типовые" теоремы, которые как следствия идут от более глобальных - вот они также как изадачи решаются типовыми методами.. . да что там говорить - даже такая казалось бы творческая область как изобретательство решается в большинстве случаев типовыми методами. . просто вы как неспециалисты думаете, что это не так.. . относительно математики - обратитесь к тем, кто закончил мехмат и он вам расскажет, что оччень даже ДА!!!. и музыка музыке рознь - воще любой набор нот кто-то уже обзовет музыкой.. . и уже машины и мультики создают и музыку пишут...

Да.
Сразу ты создаёшь логически правильный алгоритм, а затем придерживаясь его доказываешь необходимую теорему . Вот только проблема в том, что этот алгоритм может быть не единственным в условиях поставленной задачи .
Обратить внимание в первую очередь необходимо на теорию . Возьми книгу мат. анализа просмотри все доказательства, выучи (не вызубри слово в слово, а пойми, проанализируй) все определения и аксиомы и попытайся без книги доказать сам теоремы . Сразу может не получится, но со временем начнёшь понимать логику и ход мыслей. Научишся применять свои знания в необходимый момент . В математике главное опыт . А насчёт единого алгоритма, так это математика создаёт их, а не они её !!!

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