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

Может, наступила инженерная эра математики?

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

А с Lean это как будто неизбежно 1000 человек будут строить звездолёты, чтобы в космос летать, каждый отвечает за свою деталь, конвейр, контроль качества, и тд (так сейчас устроены массовые проекты у Тао и Конторовича, например).

Зачем строить звездолёты (в космос математики) непонятно, правда, но явно дешевле, чем звездолёты в настоящий космос.

кто совсем не знает Lean и готов потратить два часа на развлечение (в самом низу там ссылка на онлайн версию Lean) с ним: знать ничего не нужно, просто наводите курсор на текст или двигаете текстовый курсор и смотрите, как меняются переменные справа (я то же самое пытался в Visual Studio делать, но иногда ерунда какая-то выходила — видимо, другая версия Lean. С другой стороны, Copilot нехило так подсказывает, что вообще ничего делать не надо (когда работает). А иногда не компилится и хрен знает почему).

за два часа можно освоить как доказываются простые факты про пределы последовательностей вещественных чисел. В общем, это иллюстрация, что такое Тактики в Lean.

Я помню, таким же образом когда-то Python учил, когда сразу дают программу, и, в ней разбираясь, изучаешь язык.

с чатомЖПТ доказали формулу товарища Суня!! Я горд (мечтал об этом). Заняло примерно два часа. В принципе, идейно задача по модулю известного состояла в том, чтобы проверить, является ли данный вектор линейной комбинацией других данных векторов. Но, блин, сам я бы такой код в жизни не написал. Хотя ничего сложного в нём нет, прочитать и верифицировать-то.

Внимание, в вопросе замены.

Чтобы не «слопать это» во время разговора, лучше думать, прежде чем открывать рот. Можно «лопать» и человека, а когда «лопает», возможно, стоит обратится к врачу.

Мы спрашиваем вас, от какого греческого слова произошло «лопать». А, впрочем, достаточно и того, что вы назовете «это».

Электронная версия книги "Математики Санкт-Петербурга и их открытия", в свободном доступе.

Что главное должен воспитывать в себе ученый? Нужно избавиться от излишнего честолюбия. Не следует думать, что счастливым может быть только гений. Нужно приучиться ценить даже маленькое достижение, радоваться ему и никогда не переоценивать себя. Нужно выработать в себе трудолюбие. Нужно понять и воспитать в себе радость познания, которая почти то же, что и радость жизни. Счастье в том, чтобы дело твоей жизни было нужно людям.

С. Л. Соболев

"Ученики с мельницы не применяют свои колдовские возможности без приказа Мастера или без особой надобности (за исключением безобидных шуток). Они постоянно заняты обычной хозяйственной работой на мельнице — чистят снег, изготавливают новое мельничное колесо, заготавливают торф на зиму.
— Не пойму я, зачем работать, если всё, что мы делаем своими руками, можно просто наколдовать?!
— Всё так, — ответил Тонда, — только такая жизнь может и опостылеть. Без работы, брат, жизнь не жизнь! Так долго не протянешь!
Кроме того, на чёрную магию есть свои ограничения — иногда подмастерьям приходится трудиться, не прибегая к ней."

Тако же и нам подобает с ИИ, чтобы не сойти с ума и не попасть под власть тёмных сил окончательно.

Вау, Илья Шкредов доказал гипотезу Зарембы!!!! https://arxiv.org/abs/2603.14116

чукча не читатель, чукча писатель. ныне — чукча не писатель, чукча каюр нейросети, погонщик ИИ и укротитель промптов.

Зарешали (?) ещё одну задачу Эрдёша (там классный трэд, чат 5.2 не справлялся, а 5.4 справился). Препринт вот не очень длинный. Интересно, насколько правильно, я вот не могу проверить.

День теории игр 3 апреля.

Приглашаем вас, ваших сотрудников и студентов посетить День теории игр в пятницу 3 апреля 2026 года.

"День теории игр" (https://game.hse.ru/gtday2026) -- это научно-популярный онлайн лекторий о применении теории игр в разных главах теоретической экономики и других общественных науках. Мы расскажем о главных результатах и новых вопросах в главных разделах теории игр: аукционы, дизайн механизмов, военная наука, устройство рынков, сети, общественный выбор, дизайн информации и не только.

Встреча пройдёт онлайн, ссылку вы получите после регистрации: https://forms.yandex.ru/u/69c24ae4eb61462a814aac12

Содержание:

11:15 Приветствие

11:30-12:00 Алексей Кондратьев, ВШЭ Петербург (https://www.hse.ru/org/persons/214098890/) "Теорема Эрроу и геометрическая прогрессия"

12:00-13:00 Олег Баранов, ВШЭ Москва (https://www.obaranov.com/index.html), "Аукционы -- теория, практика и снова теория".

13:00-13:30 Алексей Савватеев, МФТИ, АГУ, ЦЭМИ РАН (https://savvateev.xyz/), "Полковник Блотто приехал на фронт со своей молодой женой".

13:30-14:00 Александр Нестеров, ВШЭ Петербург (https://www.hse.ru/staff/asnesterov), "Задача трёх тел в экономике" + Анонс летней стажировки в Лаборатории теории игр.

14:00-15:00 Арсений Самсонов, ВШЭ Петербург (https://sites.google.com/view/asamsonov) Коллективный выбор устройства информации.

15:00-15:30 Татьяна Майская, ВШЭ Москва (https://www.tmayskaya.com/) "Я ловлю, ловлю сигналы" или "Тайная ценность тяжкого труда"

15:30-16:00 Иван Самойленко, ВШЭ Москва/Петербург (https://www.hse.ru/org/persons/208522817/), "Тятя, тятя, наши сети"

16:00-16:30 Василий Гусев, ВШЭ Петербург (https://www.hse.ru/org/persons/325138730/), "Значение Шепли (для науки и мира)".

17:00-18:00 Сергей Измалков (https://www.nes.ru/about/profiles/faculty/lecturers/Sergei-Izmalkov), "Рынок такси, рынок рекламы и кое-что совсем другое".

18:00-19:00 Михаил Решетов (https://economics.ucla.edu/person/mikhail-reshetov/), "Идентификация в аукционах, макро, эконометрика и саморефлексия".


------------приложение---------------
ссылки на прошлые дни теории игр с подробностями:
день теории игр на матфаке 2022 - https://math.hse.ru/announcements/582587008.html
- лекция Сергея Измалкова "аукционы и механизмы" оттуда - https://rutube.ru/video/797474bb80d499839d6855e52aeb36c3/?r=wd
день теории игр на матфаке 2023 - https://math.hse.ru/announcements/826672843.html
день теории игр на матфаке 2024 - https://telegra.ph/Den-Teorii-Igr-na-Matfake-04-13
- полная запись (6 часов!!!) - https://www.youtube.com/watch?v=r5q0p19pv9o
день теории игр в РЭШ 2024 - https://events.nes.ru/events/v-resh-projdet-tretij-den-teorii-igr/
день теории игр на МКН СПбГУ 2024 - https://vk.com/wall-25595467_5184

30 марта 1796 Гаусс построил 17-угольник. Заметка об этом, а затем там ещё доказывают, что бесконечно много простых в прогрессиях nd+1 с помощью циклотомических многочленов, а также что сумма примитивных корней это минус функция Мёбиуса.

Пишут, что AI по имени Chebyshёv под руководством Зельманова, Концевича, Окунькова, Перельмана, Смирнова и ещё одного (неназванного) будущего филдсовского лаурета доказала гипотезу Римана. В качестве промпта использовались недавно обнаруженные черновики Чебышёва, где содержался план доказательства.

срезал. 102 минуты размышлений это рекорд. Раньше максимум 30 минут было.

Христос Воскресе!

Интересно бы применить топологический анализ данных (TDA) на игре Го (weiqi). Там явно много визуальной геометрии. В отличие от классической TDA, где просто точки, тут фишки двух цветов (или даже трёх, потому что незанятые клетки тоже важны: глаза, потенциальные глаза и тд). Так что интересная математика тоже должна появиться. Но (мне) пока непонятно, с чего начать. Просто устойчивые гомологии конкретной позиции не выглядят интересным объектом.

UPD: много про го для начинающих.