Альфу глючит?

[Ktina]

Альфочка утверждает, что не знает, является ли число $\sqrt{1+\sqrt 2}$ рациональным. Это глюк или она вправду стала резко тупеть?

[Профессор Снэйп]

Надо решать уравнение $x^4 - 2x^2y^2 - y^4 = 0$ в целых числах, однако

[Ktina]

Профессор Снэйп в сообщении #616391 писал(а):

Надо решать уравнение $x^4 - 2x^2y^2 - y^4 = 0$ в целых числах, однако

Это ещё зачем?
Там же всё очевидно (если исходить из иррациональности числа $\sqrt 2$).

[Профессор Снэйп]

Ktina в сообщении #616395 писал(а):

Это ещё зачем?
Там же всё очевидно (если исходить из иррациональности числа ).

А мне ниачивидно! Распишите, как у Вас.

-- Вс сен 09, 2012 01:10:31 --

А, ну да вообще-то... Всё слишком просто

[Ktina]

Профессор Снэйп в сообщении #616396 писал(а):

Ktina в сообщении #616395 писал(а):

Это ещё зачем?
Там же всё очевидно (если исходить из иррациональности числа ).

А мне ниачивидно! Распишите, как у Вас.

$$\sqrt{1+\sqrt 2}\in\mathbb Q\to 1+\sqrt 2\in\mathbb Q\to \sqrt 2\in\mathbb Q\to\text{противоречие}$$

[arseniiv]

Напишите письмо в Wolfram Research, пусть в алгоритм добавят. Mathematica 8 тоже не определила (немудрено, они одно и то же используют).

[Ktina]

Кстати говоря, мне не нравится классическое доказательство иррациональности корня из двух.
Вот моё:

Пусть корень из двух рационален. Тогда он равен отношению двух целых чисел, отношение квадратов которых равно двум. Но если отношение квадратов двух целых чисел равно двум, то в разложении на множители одного из этих квадратов содержится нечётное число двоек, что невозможно.

[Munin]

Ktina в сообщении #616416 писал(а):

Кстати говоря, мне не нравится классическое доказательство иррациональности корня из двух.
Вот моё:

Пусть корень из двух рационален. Тогда он равен отношению двух целых чисел, отношение квадратов которых равно двум. Но если отношение квадратов двух целых чисел равно двум, то в разложении на множители одного из этих квадратов содержится нечётное число двоек, что невозможно.

А это разве и не есть классическое?

[Ktina]

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

А это разве и не есть классическое?

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

[nnosipov]

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

А это разве и не есть классическое?

Нет, классическое гораздо лучше --- оно не опирается на основную теорему арифметики, которую не так-то просто доказать.

[xmaister]

(Оффтоп)

Ktina в сообщении #616468 писал(а):

Кроме того, моё состоит только из слов - ни одного математического символа.

А это, разве, хорошо?

[Sender]

xmaister в сообщении #618531 писал(а):

А это, разве, хорошо?

Вообще, не назрела ли необходимость создания единой международной базы математических фактов и их доказательств, представленных, к примеру, в таком виде:
http://us.metamath.org/mpegif/sqr2irr.html? В частности, в этом случае проверка корректности всякого рода сомнительных доказательств может производиться компьютером практически мгновенно.

[worm2]

Sender в сообщении #618561 писал(а):

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

Проблема в том, что сейчас доказательства (как сомнительные, так и несомненные) представлены на человеческом языке. А чтобы проверить любой программой любое доказательство, его нужно перевести на формальный язык. Работа, как Вы сами понимаете, неподъёмная. Кто будет этим заниматься? Есть ли добровольцы сделать это для более-менее сложных теорем, скажем, для основной теоремы арифметики? Вот если бы была программа сама умела с человеческого на формальный переводить...

[Sender]

worm2 в сообщении #619952 писал(а):

Есть ли добровольцы сделать это для более-менее сложных теорем, скажем, для основной теоремы арифметики? Вот если бы была программа сама умела с человеческого на формальный переводить...

Ну вот лемму Евклида осилили же. Вообще, такой перевод доказательств на формальный язык, как ине кажется, сродни программированию. Дело за высокоуровневыми языками доказательств и их компиляторами.