и там чудеса — формула для числа пи была найдена экспериментом, а потом доказана.

Из предисловия к книге "Алгебраическая алгоритмика", Ноден, П. / Китте, К.. (книга конца 80х, предлагаемый язык программирования — Ада).

Идея — что алгебру (кольца, идеалы...) можно преподавать (хотя бы прикладным математикам) сразу как набор алгоритмов (и сразу программировать), а не как набор теорем.

Я помню, как в универе вручную решали системы уравнений (4 на 4? или 5 на 5?) — единственным смыслом чего, видимо, было то, что уж совсем всех можно этому научить, а потом проверить на контрольной. И аккуратности учило.

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

"Что такое "геометрия без аксиомы параллельных линий"?-- Ребятишки забавляются тем, что прыгают на одной ноге. Быстро подвигаться вперед этим способом! они, разумеется, не могут; и передвинуться далеко, -- например, версты на две -- не могут. Но при усердии все-таки не очень медленно передвигаются на расстояния, не вовсе ничтожные: иной, прыгая, не отстает от человека, идущего тихо; и провожает его целую четверть версты. Это очень трудный подвиг. И достойный всякой похвалы. Но лишь когда это -- шалость ребенка. А если взрослый человек, -- и не для шалости, а серьезно, по своим серьезным делам, пустится путешествовать, прыгая на одной ноге, это будет путешествие не вполне безуспешное, -- нет!-- только совершенно дурацкое."

Из Чернышевского, очень понравилось.

#Lean
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.

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

Кратко, его товарищи в процессе работы, прописывая основания кристальных когомологий, обнаружили, что оригинальное доказательство не компилируется. В нём нашлась неустранимая дыра: доказательство ссылается на статью N.Roby 1965 года, Лемма 8 из которой неверна. Что удивительно, N.Roby доказывает её, неправильно цитируя свою же статью 1963 года.

Кевин пишет, что для него в этот момент обрушилось всё доказательство; теорема Ферма стала вновь стала открытой проблемой. Но он знал, что раз теория кристальных когомологий используется последние пятьдесят лет, то она работает, и нужно лишь по-новому обосновать верное утверждение.

Кевин, чем писать электронные письма экспертам, выпил кофе с одним профессором, пообедал с другим, и в конце концов нашёлся текст Артура Огуса, который закрывал дыру, а сам Артур взялся закрывать известные ему дыры в этом своём тексте.

Кевин заключает замечанием о том, в каком хрупком состоянии находится современная математика, сколько критических деталей известны лишь специалистам и нигде толком не прописаны.
--------

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

Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!

думаю, что весьма скоро компьютеры будут доказывать новые теоремы. Что породит множество интересных коллизий. Сейчас на работу берут математиков, которые смогли придумать что-то новое и интересное. А если они это делают, существенно опираясь на AI ? Как решать кто круче и кому давать гранты? Стоит ли бежать учить Lean? Или заниматься максимально далёкой от формализации математикой?

Представьте, что есть писатель, и примерно 98% текста генерится не человеком, а AI (и выходит не хуже, чем у писателей-людей. А то и лучше — промпты там лучше подобрал). Стоит ли такому человеку давать литературные премии? Такое уже есть ?(есть ли рассказы, написанные AI, которые очень хороши?)

Коллизии ограничиваются только вашей фантазией.

насколько я понимаю, китайский чатgpt - https://www.deepseek.com/ по всяким метрикам не хуже обычного. И работает в том числе из России и Китая. Вдруг кому надо.

Впрочем, как и обычный чатGPT он не смог мне найти уравнение параболы, касательной к двум данным прямым в данных точках.

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

UPD: победил параболу. deepseek стало искать наклонную параболу, но в какой-то момент решает квадратное уравнении, выбирает "for simplicity" один корень и получается двойная прямая в итоге. И признается, что не получилось. Если явно сказать, "выбери другой знак в шаге 8", то всё получается, и даже меня хвалит за подсказки.

Видел где-то когда-то изречение (как обычно, древнее и китайское):

Если тебе достался склон, сделай на нем водопад!

Источник найти не смог —- может кто-нибудь вспомнит откуда это? Чаты жпт умеют красиво галлюцинировать, откуда оно, но всё неправда. Поиск в интернете по всем цитатам с водопадами (а тут суть именно про водопад, а вместо склона может быть гора/уступ/обрыв...) — ничего не дало. Почему-то у меня оно ассоциируется с Гонконгом (может, там где-то на стене было написано?).

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

Решение красивое, не откажите себе в удовольствии его придумать. (Московская олимпиада 1958года)

Посмотрел фильм “Иду на грозу” (1965)

(драма про внутреннюю жизнь советских геофизиков).

Очень понравилось как показан эмоциональный мир учёных. Нелинейность сюжета, то есть не завязка-кульминация-[предсказуемый] финал, а несколько переплетающихся сцен со взлётами-подениями, напоминает хороший сериал (Twin peaks). Что и герой, и антигерой, скорее, оба положительные, и даже друзья, а злодеи — это окружающая среда. Как спорят — буквально, фразой-двумя всю ситуацию выворачивая наизнанку.

Закон взаимности Вейля: от теоремы Виета до квадратичного закона взаимности

(это для старшеклассников/младшекурсников). Чтобы понять половину, достаточно знать теорему Виета, а чтобы понять всё, достаточно знать немного теории Галуа.

Смотрите какая формула классная (но не моя). Можете доказать?

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

давайте вместе отсюда что-нибудь докажем?

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

много всякой красоты, если суммировать дроби по модулю p, p^2,,,

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