Как проводят свободное время философы и/или математики

[Munin]

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

Правда, в физике критерием истины в конце концов становится технология – если GPS работает, значит, ОТО верна.

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

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

"...многие люди не осознают того факта, что не понимают смысла слов, которые употребляют." (Вавилов) В том, что школьная математика с этим справляется плохо, ничего удивительного нет. Если геометрия еще худо-бедно учит рассуждать, то школьная алгебра сводится к натаскиванию на применение заученных формул, выводу которых не уделяется вообще никакого внимания.

Ну, на самом деле, алгебра учить вообще не употреблять слов, а употреблять символы, формулы и вычисления.

И добавлю, что в хорошей школе всё-таки вывод всех формул - это обязательный навык любого школьника. Кроме, может быть, самых базовых, типа $a=b\quad\Longleftrightarrow\quad a+c=b+c$ в $\mathbb{R},$ что всё-таки муторно, и начинает быть интересным только в вузовской алгебре.

[Anton_Peplov]

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

в хорошей школе всё-таки вывод всех формул - это обязательный навык любого школьника

И формулу для решения квадратного уравнения там выводят? И сумму геометрической прогрессии? И формулы двойного угла?
Если так, то среди моих знакомых нет никого, кто учился бы в хорошей школе.

[Munin]

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

И формулу для решения квадратного уравнения там выводят? И сумму геометрической прогрессии? И формулы двойного угла?

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

-- 30.12.2015 02:16:05 --

Квадратное уравнение - выделением полного квадрата. Суммы прогрессий - по методу великого Гаусса: сдвиг и вычитание. Формулы двойного угла - из более общих формул суммы углов. Из них же - суммы синусов, произведения синусов и т. п.

[Anton_Peplov]

А у меня вот до сих пор навыки вывода хромают, то минус где-нибудь забуду, то слагаемое пропущу.

-- 30.12.2015, 03:10 --

grizzly в сообщении #1086928 писал(а):

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

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

[Red_Herring]

Прежде всего формализованное доказательство минимально серьезной теоремы будет настолько длинно, что его не только записать, но и прочитать, не говоря о том, чтобы понять невозможно будет (к алгебре, возможно, это не относится). Более того, большинство публикуемых доказательств настолько формализованы, чтобы их прочитать или даже проверить на современном уровне строгости можно, а вот понять—затруднительно. Понимание это ответ не на вопрос "Как?" ("А как оно работает?"), а "Почему?" ("Почему оно работает? Какие идеи лежат в основе?"). При настоящем понимании читатель может доказывать аналогичные, но другие результаты. При механическом понимании может подкрутить винтик-другой и маргинально улучшить (при это понимания всей картины не требуется).

(Оффтоп)

Когда в нашем университете на "Farts & Swines" решили сократить семестр с 13 до 12 недель (мотивируя заботой о студентах и тем что в "Dork University" семестр 12 недель, как будто мы когда-нибудь равнялись на него), один мой молодой коллега закончивший университет как раз в последнем году с 13-неделками заявил, что он счастлив, что этого безобразия (12 неделек) ему увидеть не придётся. Именно на 13й неделе профессора расслабляются настолько, чтобы обсуждать связи и перспективы, отвечать на вопросы "Почему и зачем", а не "Как".

[arseniiv]

Надо ещё заметить, что формализованное доказательство не обязательно должно быть не организованным иерархически — не в смысле выводимости отдельных формул вывода друг из друга, а именно в делении на какие-то отдельные «подрезультаты» (не буду говорить «леммы» — в разных текстах они разной крупности) разной детализации, от outline до самых мелких деталей для формальной проверки.

Тут недавно как-то даже статью упоминали про способ записи и манипулирование такими доказательствами в традиционных статьях. Хотя, разумеется, можно сделать много лучше, не выкладывая это на линейный носитель (бумагу), т. к. тогда либо надо будет отделить друг от друга уровни детализации, либо связанные выводимостью подрезультаты разных уровней. Почти автоматически генерировать самый нижний уровень (и некоторые повыше) может proof assistant и сейчас. Короче, точные, но и доказательства в удобном математикам виде — это дело будущего. Я не очень понимаю, почему формальные противопоставляются потенциально ошибочным ясным и, соответственно, первые считаются длинными/неподъёмными, а вторые короткими. Скучный «формальный слой» пускай проверяет компьютер, идеи оставим человеку, и всё это может сочетаться в одном medium вполне нормально. Бумага и ассоциированное с ней мышление, уходите в прошлое!

[Red_Herring]

То, что arseniiv упоминает дело будущего, но в любом случае статья должна содержать и описание идей, и их имплементацию. Однако это увеличивает объём и бумажные журналы против этого. Если же говорить о чисто электронных, то они часто имитируют бумажные—и тоже против.

[Munin]

Anton_Peplov

(Оффтоп)

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

А у меня вот до сих пор навыки вывода хромают, то минус где-нибудь забуду, то слагаемое пропущу.

Эти навыки надо тренировать до автоматизма. (Если где-то проскакивают ошибки - то навыки самоконтроля, чтобы их отлавливать.)

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

Причём, как тут заметили на форуме, умственные навыки могут различаться в зависимости от тренировки на порядки сильней, чем физические.

Правда, ещё и различия между ними сильней. Одно дело - производные и интегралы, другое - векторы и матрицы, третье - скажем, группы и представления, четвёртое - топология какая-нибудь, для которой, как тут правильно заметили, часто картинки рисуют...

[Евгений Машеров]

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

И формулу для решения квадратного уравнения там выводят? И сумму геометрической прогрессии? И формулы двойного угла?
Если так, то среди моих знакомых нет никого, кто учился бы в хорошей школе.

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

[arseniiv]

У нас были все три, хотя мне не нравился геометрический «вывод» (ко)синуса суммы. Но раз уж определение было через единичную окружность, сейчас понятно, что по-другому было никак.

[Munin]

(Оффтоп)

arseniiv в сообщении #1087038 писал(а):

У нас были все три, хотя мне не нравился геометрический «вывод» (ко)синуса суммы. Но раз уж определение было через единичную окружность, сейчас понятно, что по-другому было никак.

Что-то я не понимаю, а что в нём плохого. Берём единичную окружность, пусть $\overrightarrow{OA}=\vec{\imath},$ и соответственно ориентированные углы $\measuredangle AOB=\alpha,\quad\measuredangle BOC=\beta.$ Будем использовать операцию $[\vec{v}],$ означающую поворот вектора в плоскости на $+^\pi\!/_2,$ аналогично векторному произведению в 3 измерениях, и в соответствии с обобщением векторного произведения на $n-1$ вектор в $n$ измерениях.

Тогда, разложим вектор $\overrightarrow{OC}$ по базису $(\overrightarrow{OB},[\overrightarrow{OB}])$:

$\overrightarrow{OC}=\overrightarrow{OB}\cos\beta+[\overrightarrow{OB}]\sin\beta$
$\overrightarrow{OB}=\overrightarrow{OA}\cos\alpha+[\overrightarrow{OA}]\sin\alpha$
$[[\vec{v}]]=-\vec{v}$

и  тупая  прямая подстановка даёт искомые формулы, две сразу.

В Википедии, конечно, написано что-то феерическое.

[Anton_Peplov]

grizzly в сообщении #1085865 писал(а):

Если что, то теоремы Муавра и Шредера--Бернштейна это уже совсем другие теоремы :

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

-- 03.01.2016, 18:49 --

Red_Herring в сообщении #1086944 писал(а):

Прежде всего формализованное доказательство минимально серьезной теоремы будет настолько длинно, что его не только записать, но и прочитать, не говоря о том, чтобы понять невозможно будет

Правильно ли я Вас понимаю, что:
1. Формализованное доказательство минимально серьезной теоремы невозможно даже записать.
2. Записать можно только формальные доказательства нетрудных теорем типа иррациональности $\sqrt 2$, в правильности которых никто и без формальных доказательств не сомневается.
3. Следовательно, ценность формального доказывания равна нулю?

[Red_Herring]

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

Правильно ли я Вас понимаю, что:

Речь идёт о полностью формализованном доказательстве.

[Xaositect]

А можно пример "минимально серьезной" теоремы не из алгебры? А то оценка серьезности у каждого своя.

[Anton_Peplov]

Red_Herring в сообщении #1087830 писал(а):

Речь идёт о полностью формализованном доказательстве.

Да, конечно.