🧠💻🤖 Что происходит, когда человек с самым высоким IQ в мире (220-230) рассказывает о будущем математики? Теренс Тао, австралийский математический гений и обладатель престижнейших наград, включая премию короля Фейсала, шокирует своим откровенным взглядом на союз человеческого интеллекта и ИИ. Как изменится математика, когда компьютеры начнут решать олимпиадные задачи лучше людей? Почему даже гений признает, что будущее за коллаборацией человека и машины? В этой уникальной лекции на IMO 2024 Тао раскрывает, как искусственный интеллект уже трансформирует математические исследования, и делится личным опытом использования ИИ в своей работе. Готовы ли вы узнать, почему даже для человека с IQ 220 некоторые задачи становятся проще с помощью искусственного интеллекта?
Тайм коды
Теренс Тао (IQ 220): Математика В Эпоху ИИ
00:01 Введение
- Профессор Терен Стау впервые участвовал в олимпиаде по математике в 11 лет и получил бронзовую медаль.
- В следующем году он получил серебряную медаль, а в 13 лет стал самым молодым участником, получившим золотую медаль.
- После этого он поступил в университет и больше не участвовал в олимпиаде.
00:56 Карьера и достижения
- Сейчас он профессор в Калифорнийском университете в Лос-Анджелесе.
- Он является одной из самых больших звезд олимпиады по математике и влиятельным математиком.
01:40 Доклад о машинной помощи в математике
- Доклад посвящен машинной помощи в математике и её влиянию на исследовательскую математику.
- Ранее была лекция о новом продукте Alpha-Geometry, который может отвечать на вопросы по геометрии из олимпиады по математике.
- После доклада будет презентация об олимпиаде по математике с использованием ИИ.
03:04 История использования машин в математике
- Машины используются для решения математических задач уже тысячи лет.
- Римляне использовали абакус, а современные компьютеры появились в 1930-1940-х годах.
- Во время Второй мировой войны использовались кластеры компьютеров для вычислений.
04:57 Таблицы и базы данных
- Компьютеры использовались для создания таблиц, таких как логарифмические таблицы Непера.
- Эти таблицы до сих пор используются в математических исследованиях.
- Важные результаты в теории чисел, такие как теорема о простых числах, были открыты с помощью таблиц.
07:34 Научные вычисления
- Научные вычисления используются для больших вычислений, начиная с 1920-х годов.
- Хендрик Лоренц использовал человеческие компьютеры для моделирования уравнений жидкости.
- Современные компьютеры используются для решения множества задач, включая геометрические задачи.
09:48 Решатели SAT и SMT
- Решатели SAT и SMT используются для решения логических головоломок.
- Они могут решать задачи, но сложность времени для их решения возрастает экспоненциально.
- Пример успешного применения: решение проблемы пифагоровых троек с помощью компьютера.
11:58 Компьютерное доказательство
- Доказательство требует анализа случаев до 7824.
- Пример с 7825 показывает наличие пифагоровой тройки.
- Доказательство заняло семь лет вычислений и 200 терабайт данных.
12:53 Использование компьютеров в математике
- Компьютеры используются для анализа случаев и генерации доказательств.
- Машинное обучение и нейронные сети помогают находить новые связи.
- Формальные помощники по доказательствам упрощают проверку аргументов.
15:11 Теорема о четырех цветах
- Доказательство теоремы о четырех цветах в 1976 году.
- Использовалась индукция и проверка подграфов.
- Современное доказательство использует около 700 графов и современные языки программирования.
17:54 Гипотеза Кеплера о упаковке сфер
- Гипотеза о наилучшей упаковке сфер в трехмерном пространстве.
- Стратегия тота делит пространство на политопы Воронова.
- Томас Хейлс использовал оценки для получения верхних границ плотности.
21:49 Гибкость метода и его сложности
- Метод очень гибкий, что приводит к множеству возможных оценок.
- Фергюсон изменял оценки, чтобы минимизировать функционалы, что усложняло процесс.
- В 1998 году нашли область, подчиняющуюся множеству линейных неравенств, но доказательство было сложным и потребовало использования компьютеров.
22:48 Доказательство и его формализация
- Доказательство заняло 250 страниц заметок и 3 гигабайта данных.
- Рецензирование заняло четыре года, и статья была опубликована с оговоркой.
- Проект Flyspeck формализовал доказательство за 12 лет, что укрепило уверенность в результате.
24:47 Конденсированная математика
- Петр Шульц создал теорию конденсированных групп и пространств.
- Он доказал теорему о исчезновении категориальной группы, что стало основой его теории.
- Доказательство было сложным и потребовало формализации на языке LIn.
27:14 Формализация и её последствия
- Формализация теоремы М заняла 18 месяцев и выявила незначительные технические проблемы.
- Проект пополнил математическую библиотеку LIn и разработал вспомогательное программное обеспечение.
- Был создан план для разбиения больших доказательств на мелкие шаги, что упростило формализацию.
30:33 Преобразование формальных доказательств
- Формальные доказательства преобразуются в читаемые человеком.
- Инструменты позволяют интерактивно изучать доказательства, кликая на нужные места.
- В будущем учебники могут быть написаны в интерактивном стиле.
31:31 Личный проект по формализации
- Автор начал проект по формализации задачи в коммутаторной теории.
- Доказательство заняло около 33 страниц и было формализовано за три недели.
- Проект сделал задачу доказательства более открытой и совместной, используя механизмы BluePrint.
32:57 Теория Пфр
- Теория Пфр зависит от множества предыдущих утверждений.
- Утверждения имеют разные цвета в зависимости от формализации.
- Проект позволяет независимым участникам работать над разными частями доказательства.
33:58 Сотрудничество и формализация
- Каждый участник работает над своей частью доказательства.
- Проект включает людей из разных областей, включая программистов.
- Легкий компилятор автоматически проверяет корректность кода.
35:03 Преимущества формализации
- Формализация доказательств занимает больше времени, но ускоряет процесс.
- Возможность изменения доказательств без переписывания всего текста.
- Формализация помогает выявлять и исправлять ошибки.
37:23 Машинное обучение в математике
- Машинное обучение используется для предсказания ответов на вопросы.
- Применение нейронных сетей в теории узлов.
- Узлы имеют инварианты, которые не меняются при деформациях.
38:10 Теория узлов и машинное обучение
- Узлы эквивалентны, если их можно непрерывно деформировать.
- Инварианты узлов включают сигнатуру и гиперболические инварианты.
- Машинное обучение помогает предсказывать сигнатуру узлов.
40:55 Анализ заметности
- Машинное обучение создает “черную коробку” для предсказания сигнатуры.
- Анализ заметности помогает определить важные входные данные.
- Визуальный анализ графиков помогает делать предположения и исправлять гипотезы.
42:48 Большие языковые модели
- Машинное обучение дает подсказки о связях в математике.
- Большие языковые модели, такие как GPT-4, достигают результатов на уровне человека.
43:29 Модель ChatGPT и её возможности
- ChatGPT успешно решил задачу из IMO 2022 года.
- Уровень успеха в решении задач IMO составляет около 1%.
- Модель решает задачи, которые людям кажутся сложными, но часто ошибается в простых задачах.
44:19 Проблемы и улучшения в использовании ИИ
- ИИ может легко справляться с задачами, которые людям даются с трудом.
- Модель угадывает результат арифметического вычисления, но иногда ошибается.
- Продолжаются работы по улучшению точности и надежности ИИ.
45:22 Применение ИИ для решения задач
- ИИ можно использовать для решения задач, передавая их на обработку Python.
- Языковые модели могут выдавать только правильные ответы.
- Люди пробуют различные подходы для решения математических задач.
46:38 ИИ как муза и помощник
- ИИ может быть полезен как собеседник и источник идей.
- Пример: использование генерирующих функций для решения задачи.
- ИИ помогает в написании формальных доказательств, предлагая возможные шаги.
49:00 Будущее ИИ в математике
- ИИ может помочь в решении узкоспециализированных задач.
- Надежда на генерацию хороших гипотез и создание связей между математическими объектами.
- Будущее математики с использованием ИИ будет захватывающим.
52:30 Вопросы и ответы
- Обсуждение формализации математики и теории типов гомотоий.
- Важность автоматического перевода доказательств между языками.
- Важность разнообразия подходов к формализации математики.
55:53 Наставники и поступление в университет
- У меня были хорошие наставники в школе, на уровне бакалавриата и магистратуры.
- Поступление в университет не должно быть обязательным, важно быть готовым.
- Я поступил в университет в 13 лет, что было удобно из-за близости к дому.
- Опыт поступления в молодом возрасте зависит от многих факторов.
57:11 Выбор тем исследования
- В начале карьеры наставники предлагали задачи, сейчас это происходит случайно.
- Математика — это социальная деятельность, и многие вопросы возникают из бесед с другими математиками.
- У меня есть долгосрочные проекты, но часто новые вопросы возникают в ходе общения.
- В будущем людям нужно будет быть более гибкими и перемещаться между темами.
- Следующий докладчик — Саймон Койл из X-X, который расскажет об олимпиаде по математике с использованием ИИ.
https://browser.yandex.ru пересказ текста
Расшифровка видео
Профессор Теренс Тао: от вундеркинда до математической звезды
0:01
Здравствуйте Всем здравствуйте Здравствуйте всем Некоторые из вас Дорогие участники
0:11
очень молоды Возможно вы не знаете кто такой профессор теренс Тао поэтому несколько слов для
0:21
знакомства он впервые участвовал в Олимпиаде по математике когда ему было 11 лет и получил
0:30
медаль в следующем году он вернулся и получил серебряную медаль после этого
0:37
в возрасте 13 лет он получил золотую медаль и стал самым молодым участником получившим
0:44
золотую медаль потом он не знаю заскучал и пошёл в университет и он больше не участвовал
0:54
в Олимпиаде по математике теперь он профессор в калифорнийском университете в лос-анджелесе
1:01
и э и я могу сказать что он определённо самая большая звезда олимпиады по математике и конечно
1:11
один из самых влиятельных математиков нашего времени Особенно для вас профессор теренс Тао
Олимпиада была одним из самых весёлых периодов в моей жизни
1:40
Спасибо я очень рад быть снова здесь на олимпиаде по математике время проведённое на Олимпиаде было
1:46
одним из самых весёлых периодов в моей жизни я до сих пор с теплотой вспоминаю об этом Я надеюсь что всем нам было весело на соревнованиях независимо от того получили ли вы хороший балл
1:55
или нет но и на социальных мероприятиях здесь всегда проводят хорошие мероприятия здесь Проходит очень хорошее э мероприятие ээ мой доклад посвящён и и более широко машинной
Революция ИИ в математике: от Alpha Geometry до исследований
2:08
помощи в математике Итак вы все слышали об и и о том как он меняет Всё я думаю что сегодня ранее
2:14
была лекция от Deep Mind о том как они выпустили новый продукт Alpha Geometry который Теперь может
2:21
отвечать на некоторые вопросы по геометрии из олимпиады по математике и сразу после моего выступления будет презентация об олимпиаде по математике с использованием и и оставайтесь
2:30
после хорошо Итак я буду говорить больше о том как эти инструменты начинают изменять
2:36
исследовательскую математику которая отличается от соревновательной математики вместо того чтобы
2:42
иметь 3 часа или сколько-то ещё для решения задачи вы тратите месяцы и иногда вы не решаете
2:47
задачу тогда Вам приходится менять задачу это определённо не то же самое что математические
2:52
соревнования хотя есть некоторые пересечения в навыках Так что это всё очень захватывающе и это начинает быть преобразующим но с другой стороны также существует ощущение
3:01
преемственности мы на самом деле уже давно используем компьютеры и машины для решения
3:09
математических задач и Просто природа того как мы это делаем меняется но это действительно
3:15
продолжает долгую традицию машинной помощи хорошо вот вопрос как М как долго мы используем
История машин в математике: от древнего абакуса до современных компьютеров
3:24
машины для выполнения математических расчётов и ответ ты лет я имею в виду
3:30
Вот машина которую Римляне использовали для математики хорошо абакус на ранних машинах есть даже некоторые более ранние ладно это довольно скучно хорошо Это не очень умная машина
3:39
А как насчёт компьютеров Как долго мы используем компьютеры для решения математических задач это
3:44
примерно 300-400 лет я думаю это немного странно потому что наши современные компьютеры электронные
3:50
компьютеры появились только в 1930 и 194 годах но компьютеры не всегда были электронными до
3:57
этого они были механическими а до этого они были человеческими компьютер на самом деле
4:03
был профессией человеком который выполняет вычисления вот кластер компьютеров во время Второй мировой войны чтобы вычислять баллистик и другие вещи у них был целый кластер компьютеров в
4:15
основном состоящий из девушек потому что мужчины воевали а также использовались арифмометры и были
4:21
программисты которые в основном просто говорили девушкам что делать и вы знаете
4:27
основной единицей лите мощности в то время была не ЦП а кило девочка это килогерц вое время так
4:35
что сколько вычислений вы можете сделать Дися девушек работающих так в течение одного часа но
4:41
мы на самом деле использовали компьютеры даже раньше как я уже сказал с 1700 годов или даже
4:47
раньше самое основное использование компьютеров в те времена заключалось в составлении таблиц вы
4:54
возможно слышали о логарифмических таблицах непера если вам нужно было вычислить синус и
4:59
и так далее ти вы использовали компьютер для генерации этих огромных таблиц когда я ещё учился в средней школе мы всё ещё в нашей Учебной программе изучали Как пользоваться этими таблицами
5:09
которые только начинали выходить из употребления потому что теперь у нас есть калькуляторы и компьютеры мы всё ещё используем таблицы сегодня в математических исследованиях мы полагаемся
5:20
на таблицы мы называем их базами данных сейчас но на самом деле это всё тоже самое Существует
5:25
множество важных результатов в математике которые были впервые открыты с помощью таблиц
5:31
в теории чисел одним из самых фундаментальных результатов является теорема о простых числах
5:36
он примерно показывает сколько простых чисел существует до Большого числа X и был открыт лигандрол своего рода компьютером который вычислят таблицы первых миллиона простых чисел
5:53
и пытался найти закономерности а затем через пару веков появляется ещё одна действительно важная гипотеза таким образом это было в конечном итоге Доказано примерно в 1907 году но есть ещё
6:05
одна действительно Центральная проблема в теории чисел называемая гипотезой Бернарда свинторжицкий кривых Таблица которую сейчас используют многие математики включая меня
6:23
называется Онлайн энциклопедия целочисленных последовательностей Возможно вы а сами с этим
6:28
сталкивались Так что вы можете узнать многие последовательности целых чисел
6:34
просто по памяти Например если я скажу вам последовательность 11 2 3 5 8 13 Вы знаете
6:40
что это такое Это последовательность фибоначи и О это база данных сотен тысяч последовательностей
6:46
подобных этой и часто Когда математик работает над исследовательской задачей существует какая-то
6:52
естественная последовательность чисел связанная с ней возможно существует последовательность про
6:59
от N и вы вычисляет размерность или мощность множества или что-то в этом роде и вы можете
7:06
вычислить первые пять или шесть из этих чисел или 10 из этих чисел а затем сравнить их с и если вам
7:13
повезёт эта последовательность уже была найдена кем-то другим и она была обнаружена из совершенно
7:19
другого источника связанного с изучением какой-то другой математической проблемы и это действительно
7:26
даёт вам большой намёк на то что существует связь между двумя проблемами и таким образом возникло
7:31
много многообещающих продуктивных исследований Итак таблицы один из самых ранних способов
Три способа, которыми компьютеры меняют математику
7:38
которыми мы пользовались компьютерами Когда вы думаете о том как использовать компьютеры для решения математических задач вы в первую очередь представляете себе обработку чисел официальное
7:48
название этого процесса научные вычисления Итак вы просто хотите сделать очень большие вычисления
7:53
и вы просто выполняете много-много арифметики передавая это компьютеру и мы делаем Это с 1920
7:59
годов возможно первым человеком который действительно сделал научные вычисления был хендрик Лоренс ему было поручено я думаю голландца выяснить Что произойдёт Они хотели построить
8:10
действительно гигантскую дамбу дамбу Арис и им нужно было узнать что произойдёт с потоком воды
8:16
Итак им пришлось смоделировать некоторые уравнения жидкости для этого он использовал целую группу
8:22
человеческих компьютеров чтобы это вычислить ему пришлось изобрести арифметику с плавающей запятой
8:28
чтобы сделать это Таким образом он понял что если вы хотите чтобы много людей выполняло много вычислений очень быстро Вам следует представлять множество чисел разных порядков как числа с
8:37
плавающей запятой э Конечно мы теперь используем компьютеры для моделирования всевозможных вещей
8:45
вы решаете множество линейных уравнений или уравнений в частных производных вы хотите подсчитать некоторые комбинаторные вычисления вы также можете решать алгебраические задачи таким
8:57
образом в принципе все геометрические задачи Ну не совсем всё но многие из геометрических задач которые вы видите на Олимпиадах могут быть решены в принципе с помощью научных вычислений существует
9:06
алгебраические пакеты которые могут решать задачи Вы можете превратить любую геометрическую задачу
9:12
скажем связанную с десяти точками и некоторыми линиями и окружностями в систему уравнений с двадцати действительными переменными и двадцати неизвестными и просто ввести это в Sage или
9:23
mle или что-то подобное К сожалению как только размер достигает определённой величины сложность
9:28
становится экспоненциальной или даже двойной экспоненциальной и до недавнего времени не было
9:33
действительно целесообразно просто решать эти задачи с помощью стандартных пакетов компьютерной алгебры но теперь с помощью ии Возможно это более многообещающе Так что вы
9:44
слышали об этом доклад сегодня утром ещё один тип научных вычислений который стал довольно
9:53
мощным это так называемые решали сад решали удовлетвори они предназначены для решения
10:00
по сути логических головоломок предположим У вас есть 10 утверждений или 1.000 которые могут быть
10:06
истинными или ложными если третье утверждение истина а шестое истина то седьмое будет ложным
10:11
И если вы задали целый ряд таких ограничений то сад Серебро попытается собрать всю эту
10:17
информацию и сделать вывод Можете ли вы доказать определённую комбинацию этих предложений или нет
10:22
а затем есть более сложная версия решатель сад называемая решатель удовлетвори мости Где у вас
10:29
также есть некоторые переменные X и Z и вы предполагаете некоторые законы например возможно
10:34
существует операция сложение и сложение является коммутативный и ассоциативным и вы подставляется
10:40
эти законы а также некоторые другие факты и пытаетесь просто с помощью грубой силы
10:46
вывести какое-то заключение из конечного набора гипотез Это довольно мощно но к сожалению они
10:53
также плохо масштаби сложность времени для их рения И как только вы проходите отметку
11:01
в 1000 или около того предложений становится действительно действительно сложно для этих
11:08
решатель могут решать некоторые задачи Так что один недавний успех например вот Задача
11:17
В комбинаторике которая вероятно будет решена только с помощью компьютера Я думаю что это будет
11:23
невозможно решить человеку без посторонней помощи это касалось так называе проблема пифагоровых
11:30
троек которая оставалась нерешенной до вычисления на этом большом компьютере салва Итак вопрос в том
11:38
что вы берёте натуральные числа и раскрашивается их в два цвета красный или синий и вопрос в том
11:44
Правда ли что независимо от того как вы раскрасить эти Два натуральных числа один из цветов
11:49
обязательно должен содержать пифагоровы тройку ABC три числа которые образуют размеры например 3 4 5
11:58
Итак это не было известно как истинное у нас нет человеческого доказательства этого но у нас есть
12:03
компьютерное доказательство теперь известно что на самом деле вам не нужны все натуральные числа вам нужно дойти только до се 824 несмотря на то Сколько способов Вы можете использовать чтобы
12:14
раскрасить 7.000 824 на два цветовых класса один из них будет содержать пифагоровы тройку теперь
12:20
существует два в степени 7824 таких классов вы не можете сделать это грубой силой поэтому вам нужно
12:26
быть немного умнее Но это возможно и затем Если вы хорошо с этим м мм и затем если 7 8 2 5 Извините
12:34
как только у вас есть 7 8 2 5 у вас Обязательно должна быть пифагорова тройка есть пример 7 8 2
12:41
4 где нет пифагоровы тройки ни в одном классе это можно доказать на самом деле я думаю что на тот
12:47
момент это было самое длинное доказательство в мире я думаю что это Теперь второе по длине
12:52
Доказательство доказательство потребовало 7 лет вычислений на цпу и сгенерировал сертификат доказательства таким образом само доказательство имеет длину 200 траб Хотя оно С тех пор было
13:02
сжато до всего лишь 86 ГБ м так что это один из способов которым мы используем компьютеры
13:10
просто чтобы Проводить по сути огромный анализ случаев Так что это довольно очевидный способ
13:15
использования компьютеров но в последние годы мы начинаем использовать компьютеры более креативными
13:21
способами Итак существует три способа которыми компьютеры используются для решения математических
13:27
задач и я считаю их действительно захватывающими особенно когда они комбинируются друг с другом
13:33
и с более классическими базами данных таблицами и символическими вычислениями научными вычислениями
13:40
Итак прежде всего мы используем машинное обучение и нейронные сети чтобы обнаружить новые связи и
13:47
выяснить Каким образом различные типы математики коррелируют так как это невозможно увидеть
13:52
человеку или маловероятно увидеть человеку в частности существуют большие языковые модели
13:57
которые в некотором смысле являются очень большими версиями алгоритмов машинного обучения они могут
14:04
обрабатывать естественный язык такие как чат gpt и облачные технологии и так далее и они а
14:10
иногда могут генерировать а возможные подходы к задачам которые иногда срабатывают а иногда
14:16
нет вы увидите Немного больше примеров этого на лекции после моей но есть также другая технология
14:22
которая только начинает становиться доступной для повседневного математика а именно формально
14:29
помощники по доказательствам Итак это языки языки программирования которые вы привыкли использовать
14:35
для написания исполняемого кода программ которые выполняют определённые действия формальные ассистенты доказательств это языки которые вы пишете чтобы проверять вещи чтобы
14:45
удостовериться что определённый аргумент действительно верен и действительно приводит вас к выводу На основе данных и до недавнего времени Их использование было довольно неудобным
14:54
Теперь же они становятся относительно простыми в использовании и они способствует множеству
15:00
интересных математических проектов которые не были бы возможны без этих помощников в доказательствах
15:05
и в будущем они будут очень хорошо сочетаться с другими инструментами которые я описал здесь Итак
15:11
я хочу поговорить о более современных способах использования машин и компьютеров для решения
15:18
математических задач Я думаю что я начал с помощи в доказательствах Да так что первое действительно
Легендарная теорема о четырёх цветах: первое компьютерное доказательство
15:25
компьютерное доказательство возможно в истории было доказательство ремы о четырёх цветах каждую
15:30
плоскость или карту можно раскрасить используя только четыре цвета это было Доказано в 1976 году
15:38
это было до появления помощи в доказательствах в настоящее время это вряд ли можно назвать
15:43
компьютерным доказательством это доказательство которое представляло собой массивные вычисления
15:49
половина из которых Была выполнена компьютером а половина людьми способ которым они доказали
15:54
теорему о четырёх цветах заключается в том что вы по сути используете индукцию по количеству стран и показываете что если у вас есть огромная карта существует некоторый
16:03
подграф стран существует список производителей из 10 2000 подграф и каждый большой Граф стран
16:10
должен был содержать один из этих подграф это была одна из вещей которые им проверяли чтобы убедиться
16:16
что подграф можно заменить чем-то более простым и раскрасить в четыре цвета вы могли раскрасить
16:22
главное И вам нужно проверить эти свойства Я думаю их называют disability и reducibility
16:29
для каждого из этих 1000 графов я думаю что одну из этих задач Они могли бы выполнить
16:35
с помощью компьютера Хотя это был компьютер 1970 годов Я думаю что им приходилось вводить
16:41
каждый Граф вручную в эту программу и проверять его другая задача на самом деле выполнялась человеком компьютером одна из дочерей одного из авторов на
16:49
самом деле потратила часы и часы на ручную проверку я думаю это связано с вопросом редуцируется был не идеальным было много мелких ошибок и им приходилось обновлять таблицу Да так
17:04
что это не было по современным стандартам компьютерным доказательством проверяемым
17:09
компьютером это стало известно гораздо позже в девяностых годах когда был предложен более простой доказательство использующее всего около 700 графов но теперь все вещи которые нужно
17:19
проверить представляли собой очень точный чётко определённый список свойств и вы могли бы написать
17:24
код на вашем любимом языке программирования C или Python или чем-то ещё и вы могли бы проверить это
17:29
на нескольких страницах в нескольких сотнях строк кода за несколько минут на современном компьютере
17:36
Извините а затем чтобы действительно проверить это полностью предоставить доказательство которое
17:42
опускается до аксиом математики это было сделано в 2005 году с использованием языка поддерживающего доказательства называемого Кох Я думаю что теперь он переименован в рож Так что это
17:55
было одно из первых доказательств и вы видите что существует огромный разрыв между тем когда доказательство впервые появилось И тем когда мы действительно смогли полностью его проверить с
18:04
помощью компьютера э другой известный пример – это гипотеза кеплера о упаковке сфер это действительно
Гипотеза Кеплера: как упаковать сферы наиболее эффективно
18:11
старая гипотеза кеплера из XV века её очень легко сформулировать вы берёте целую кучу единичных
18:18
сфер И хотите как можно эффективнее покрыть трёхмерное пространство существует довольно очевидный способ попытаться упаковать сферы это треугольная упаковка Извините как вы упаковывает
18:29
в продуктовом магазине существует также двойная упаковка называемая кубической упаковкой которая
18:34
имеет такую же плотность Итак плотность составляет около 74 про Что является очевидной упаковкой и
18:40
вопрос в том Является ли это наилучшим возможным вариантом и это оказывается удивительно сложной
18:47
задачей в двух измерениях показать что гексагональная упаковка является наилучшей не так уж сложно Только совсем недавно в восьмом и двадцать четвёртой измерениях мы узнали ответ
18:57
есть замечательная работа возможно она говорила об этом вчера но три – это единственный другой случай
19:04
о котором мы знаем кроме один который триале но да это было удивительно сложно доказать снова не
19:11
было полностью читаемого человеком доказательства этой гипотезы существует стратегия Итак конечно
19:17
Проблема в том что этих сфер бесконечно много и плотность является асимптотической величиной
19:24
это не конечная задача которую можно просто бросить на компьютер но вы може
19:30
попытаться свести её к конечной задаче Итак в пятидесятых годах была предложена стратегия тота
19:36
Каждый раз когда у вас есть упаковка она делит пространство на эти многогранники называемые
19:42
областями Воронова Так что области Воронова полито сферы – это все точки которые находятся ближе
19:48
к центру этой сферы чем к другим сферам таким образом вы можете разделить пространство на все эти потопы и у этих потопов есть определённые объёмы вы также можете подсчитать их лица
19:58
их площади поверхности и так далее И у них всех есть эти статистические данные плотность упаковки
20:04
очень тесно связана со средним объёмом этих областей Если вы сможете сказать что-то о том
20:11
как эти объёмы Политов ведут себя в среднем то вы сможете получить по крайней мере какую-то верхнюю
20:18
границу на то насколько эффективными могут быть эти упаковки и вы можете попытаться установить
20:25
связи между этими полипами очень большой Возможно это заставляет соседние быть очень маленькими Да
20:32
и возможно вы можете попытаться найти некоторые неравенства связывающие объём одного барона с
20:38
другим Итак возможно вам стоит собрать множество этих неравенств а затем сделать какую-то линейную программу или что-то в этом роде и надеюсь вы сможете вывести правильную границу этого
20:48
волшебного числа p32 которое является правильной плотностью А из всех этих неравенств люди пытались
20:55
это сделать было много попыток некоторые даже заявляли о Успехе но ни одна из них не была
21:00
принята в качестве настоящих доказательств м таким образом проблема в конечном итоге была
21:08
решена Томасом хелсон и его соавторами Итак он использовал в основном ту же стратегию но с
21:16
множеством технических доработок Он изменил ячейки с ячеек ронова на Немного более сложные ячейки и
21:22
вместо того чтобы брать объём он изобрел нечто Что называется оценкой которую вы присваивает каждой из этих я это объём плюс-минус множество мелких произвольных корректировок но снова с целью
21:35
попытаться создать все эти линейные неравенства между этими различными оценками и в конечном итоге
21:42
получить верхние границы плотности а также Надеюсь точно достичь оптимальной плотности Итак это очень
21:50
гибкий метод он даже Слишком гибкий так как есть слишком много вещей которые можно попробовать Существует множество способов установить оценку и так далее Итак здесь есть цитата сэми Фергюсон был
22:01
автором этой цитаты Извините я забыл имя так вот Фергюсон понял что каждый раз когда он сталкивался
22:06
с проблемами при попытке минимизировать свои функционалы и так далее он мог просто изменить оценку и попробовать снова но затем все вещи которые они уже проверили им пришлось
22:18
переделать и функция оценки становилась всё более сложной Я думаю что они работали над этим почти
22:23
десятилетия и это становилось сложным Но с каждым изменением мы сокращались работы это бесконечное
22:29
вмешательство не пользовалось популярностью среди наших коллег когда Я выступал на конференции я минимизировать это требовало возвращения и исправления предыдущих статей ээ но в
22:46
конечном итоге они это сделали в 198 году они объявили что наконец нашли область которая
22:53
подчинялась множеству линейных неравенств в 150 переменных которые они минимизировать
22:58
и получили свой результат изначально они не планировали сделать это доказательство с помощью компьютера но по мере усложнения проекта это стало неизбежным им приходилось использовать
23:08
всё больше и больше компьютеров Да так что доказательство было огромным по стандартам 1998 года Это было 250 страниц заметок и 3 гиб компьютерных программ и данных на самом деле у
23:20
него было очень трудно пройти рецензирования Да его отправили в один из лучших журналов по общей
23:25
математике в журнал по аналитической математике и да на рецензирование ушло 4 года с участием панели
23:31
из ДТИ рецензентов в конце они сказали что на 99% уверены в правильности доказательства но не могли
23:37
подтвердить правильность компьютерных расчётов и они сделали очень необычную вещь на самом деле они опубликовали статью с небольшим оговоркой от редакторов в которой говорилось об этом с тех пор
23:47
они на самом деле убрали эту оговорку в то время было гораздо больше споров о том квалифицируется ли доказательство с помощью компьютера как настоящее доказательство теперь я думаю мы
23:57
гораздо более комфортно к этому относимся м э Но даже после его публикации оставались сомнения в
24:04
том Действительно ли это было доказательство таким образом это возможно была первая крупная
24:28
цели он назвал это проектом фй Pack он оценил что потребуется 20 лет чтобы формализовать его
24:35
доказательства Но на самом деле с помощью двадцать первого соавтора он а в конечном
24:41
итоге завершил работу всего за 12 лет и она Наконец появилась в 2014 году Э хорошо Итак
24:49
Теперь у нас есть полная уверенность в этом конкретном результате Но это было
24:55
довольно болезненно Итак переходя К последним нескольким годам мы теперь разработали более
25:02
эффективный рабочий процесс для того как формализовать это всё ещё утомительно но
25:08
Становится лучше так что Пётр шульце который является очень выдающимся молодым математиком
25:13
например был медалистом он знаменит многими многими вещами но он создал эту удивительную
25:21
многообещающие конденсированной математикой она использует мощь алгебры теории категорий
25:29
и все инструменты алгебры для применения к функциональному анализу теории пространств
25:35
функций таких как пространство и так далее к методам которых анализ действительно был
25:41
устойчив но эта область математики в принципе могла бы позволить решать вопросы по крайней мере
25:49
в функциональном анализе а также определённые типы вопросов с помощью алгебраических методов поэтому
25:54
он создал категорию вещей это конденсированные группы и векторные пространства объяснить что
26:00
означает конденсированный заняло много времени м да он действительно так считает в основном его тезис заключается в том что все наши категории функциональных пространств
26:09
которые мы изучаем на аспирантский курсах неверны они не являются естественными это пространство с лучшими свойствами м но э итак он разработал эту теорию но ему нужно было доказать
26:21
одну очень важную теорему о исчезновении я изложил её здесь Но не собираюсь объяснять
26:28
Что означают эти символы м символы означают м но произошло очень техническое исчезновение
26:35
определённой категориальной группы которую Ему нужно было вычислить и без этого вся теория не
26:44
имеет никаких интересных последствий Так что это было своего рода основанием его теории поэтому
26:51
он написал блогпост об этом результате Он сказал что провёл целый год Одержимые доказательства этой
26:58
теоремы почти с ума сходя от этого в конце концов нам удалось изложить Аргумент на бумаге но никто
27:04
не осмелился Взглянуть на детали этого Поэтому у меня всё ещё остаются сомнения с этой теоремой
27:09
надежда на то что эта сжатая формализация может быть успешно применена в функциональном анализе зависит от её успешности эта теорема имеет крайне фундаментальное значение поэтому быть уверенным
27:18
на 99% недостаточно Он сказал что рад видеть много учебных групп по конкурсной математике
27:24
Но все они остановились на доказательстве этой теоремы доказательства не очень увлекать он говорит что это может быть его самое важное достижение на сегодняшний день лучше убедиться
27:33
что это правильно Поэтому он также был очень мотивирован чтобы чтобы формализовать эту теорему теперь на более современном языке используется язык доказательства называемый
27:42
Лин таким образом Лин это язык который был значительно развит в последние годы существует
27:48
краудсорсинга инициатива по разработке этой обширной математической библиотеки поэтому вместо того чтобы выводить все из аксиом математики что становится очень утомительным по
27:58
углубления в более сложные темы этот тип математики является очень продвинутым Итак в Lin есть Центральная математическая библиотека которая уже доказало множество промежуточных
28:08
результатов таких как те вещи которые вы могли бы увидеть скажем на курсе математики для бакалавров
28:13
например фундаментальный анализ или основные вещи такие как Теория групп или топология и так далее
28:18
эти результаты уже были формализованы и у вас есть устойчивая база вы начинаете примерно с уровня
28:23
бакалаврской математики есть большая разница между вашим текущим и целевым уровнем Но это помогает м
28:30
да Но для того чтобы это формализовать им пришлось добавить много лишнего поэтому математическая библиотека была неполной она всё ещё неполная Существует множество областей математики которые
28:42
необходимо добавить в эту библиотеку но всего за 18 месяцев им удалось формализовать эту теорему
28:49
м так и доказательство было в основном правильным были некоторые незначительные проблемы Но ничего
28:59
действительно серьёзного не было обнаружено они нашли несколько приятных упрощений были некоторые технические шаги которые было Слишком сложно формализовать и поэтому им пришлось найти
29:08
некоторые обходные пути Но на самом деле ценность этого проекта была более косвенной во-первых они
29:16
значительно пополнили математическую библиотеку Лин теперь эта математическая библиотека может обрабатывать множество абстрактной алгебры в гораздо большей степени чем раньше но также было
29:26
разработано другое вспомогательное программное обеспечение которое начали использовать будущие проекты формализации включая Некоторые из тех которые я делал таким образом например одним
29:36
из инструментов который был создан в ходе этого проекта является то что называется планом таким
29:41
образом взять огромные 50 страниц доказательства и пытаться напрямую его формализовать действительно
29:49
болезненно вам нужно держать всё доказательство в голове но что мы поняли так это то что правильный
29:54
рабочий процесс заключается в том что вы берёте большое доказательство сначала пишете то что называется черновиком который разбивает это доказательство на сотни маленьких шагов каждый шаг
30:04
Вы можете формализовать отдельно а затем просто объединяется их всё вместе Итак вы пытаетесь
30:09
разбить огромный огромный Аргумент на множество мелких частей Сначала вы пишите это а затем
30:15
разные люди в вашей команде могут формализовать разные части различных этапов вашего аргумента
30:21
таким образом они также как Побочный продукт этой формализации написали этот очень хороший план Если вы действительно хотите прочитать доказательства как человек То вероятно лучше всего обратиться к
30:32
чертежу ещё одним следствием является формальное доказательства из тысяч строк предпринимаются
30:38
усилия чтобы попытаться преобразовать его обратно в читаемое человеком доказательство ещё одной
30:43
разработкой стали инструменты которые позволяют взять доказательство написанное скажем на языке
30:48
Лин Вот пример где представлено доказательство топологической задачи и они преобразовали его
30:56
обратно в читаемое челове доказательство таким образом Весь этот текст здесь это доказательство
31:01
сгенерированного доказательства оно выглядит как человеческое доказательство используется
31:07
тот же математический язык но оно гораздо более интерактивное Вы можете кликнуть на любое место
31:12
Я не могу это сделать это статический PDF но вы можете нажать здесь где вы находитесь гипотезы
31:18
что доказываете какие переменные если есть шаг который слишком короткий Вы можете его расширить
31:23
и он объяснит откуда он взялся и вы можете дойти до аксиом Если хотите я думаю это Это замечательно и в будущем учебники будут написаны в этом интерактивном стиле Сначала вы их формализуются
31:32
быть гораздо более интерактивные учебники чем сейчас вдохновлённый этим я сам начал проект
31:40
по формализации в прошлом году я решил задачу в области коммутатор теории с несколькими людьми
31:46
включая Тима госа который здесь в аудитории Так что э Задача в области коммутатор най теории не
31:52
так уж важно В чём заключается проблема Ладно есть под множество проблемы хорошо
31:58
группы энергии 2 Итак подумайте о Z по модулю 2 в степени N как о том что называется кубом
32:03
хэмминга и он подчиняется протоколу называемому малым удвоением затем есть определённый предел
32:08
того насколько большим он может быть хорошо но на самом деле не имеет значения Каково утверждение Но это распространённая ошибка в утверждении мы это доказали доказательство занимает около
32:19
33 страниц и мы формализовать это в и там было относительно Рекорда Вероятно это всё ещё самое
32:26
быстрое формализованное научная работа выполненная за 3 недели в групповом проекте из примерно 20
32:34
человек используя все эти механизмы blueprint которые были разработаны в проекте шорса В общем
32:41
это делает задачу доказательства вещей гораздо более открытой и совместной и вы получаете все
32:49
эти красивые визуализации Итак как я уже сказал первое что вы делаете Это берёте вашу большую
32:54
теорему и разбивает её на множество маленьких частей Итак теория которую мы имеем называется ПФР
33:00
я не буду объяснять почему Это соответствует этому маленькому пузырь внизу этого графика а затем мы
33:08
вводим все эти другие утверждения таким образом доказательство pfr должно зависеть от нескольких
33:14
других предыдущих утверждений и эти утверждения также зависят от предыдущих Так что существует
33:19
Граф зависимостей и они имеют разные цвета в зависимости от того формализованы пузырь – это
33:26
утверждение которое вы уже формально доказали на своём языке синяя пузырь – это тот который ещё не
33:32
был формализованного к формализации как будто все определение на месте кто-то должен просто
33:37
это сделать белый пузырь даже само утверждение ещё не было формализована кто-то должен написать это утверждение таким образом вы получаете это дерево задач и красота этого проекта заключается
33:50
в том что вы можете заставить всех этих людей Независимо сотрудничать над разными частями
33:55
этого графика э а каждая маленькая пузырька соответствует какому-то утверждению и вам
34:02
не нужно понимать все доказательства чтобы просто работать над своей маленькой частью Итак это была проблема в комбинаторике Но люди которые внесли свой вклад были из области вероятности были даже
34:12
люди которые не были математиками а компьютерными программистами но они просто очень хорошо
34:18
справлялись с этими маленькими головоломками Итак каждый просто выбрал одну вещь один пузырь который
34:24
по их мнению Они могли сделать и они это сделали и Да за неделе мы сделали Всё это был действительно
34:30
захватывающий проект в математике Мы обычно не сотрудничаем С таким количеством людей знаете
34:37
может быть пять человек это максимум с которым я обычно сталкивался Дело в том что когда вы
34:43
сотрудничаете над большим проектом Вы должны доверять что математика каждого Верна А при определённом размере это просто невозможно но с таким проектом этот лёгкий компилятор
34:52
автоматически проверяет вы не можете загрузить ничего что не компилируется это будет отклонено
34:57
Так что вы можете сотрудничать с людьми которых вы никогда не встречали раньше м и так далее эм Да я
35:04
встретил много людей я на самом деле написал много рекомендательных писем выходя из этого
35:09
проекта да Это пример это как одна маленькая часть доказательства вот как выглядит доказательство в
35:18
Лин я имею в виду если вы знаете язык оно читаемо для человека но выглядит немного необычно Да но
35:28
это действительно разделяет задачу доказательства на множество различных несвязанных навыков есть
35:33
люди которые видят общую картину и организуют вещи на маленькие части А есть люди которые не обязательно знают всю математику но могут работать над маленькими частями по очереди Я
35:44
думаю что это будет всё более распространённый способ заниматься математикой в будущем это
35:50
всё ещё болезненно делать инструменты на самом деле не они становятся лучше
35:57
и более удобными для пользователей но всё равно нужно иметь определённые знания в программировании я бы сказал что формализовать доказательства занимает возможно в 10 раз больше времени А чем
36:07
написать его вручную с другой стороны если вы хотите изменить доказательства например в этой
36:13
теореме появилось число 12 Позже Мы улучшили это 12 до О мы получили более сильную теорему Если вы
36:20
это делаете вам нужно переписать доказательства или вы могли бы вырезать и вставить 12 в 11 Но тогда вам нужно проверить что вы не сделали никаких ошибок когда это делали когда мы это
36:29
формализовать всего несколько дней чтобы изменить 12 на 11 мы просто изменили 12 на
36:37
11 где-то и затем компилятор пожаловался как минимум в пяти разных местах теперь определённая очень конкретная часть группы не работала и мы могли просто сделать некоторые
36:46
целенаправленные исправления таким образом на самом деле уже для некоторых специфических
36:52
типов выполнение математики формальный подход оказывается быстрее В настоящее время существует
36:58
довольно много крупных проектов по формализации доказательств самый крупный проект принадлежит
37:04
Кевину базар Он только что получил большой Грант на формализацию последней теоремы ферма в Лин он
37:10
говорит что на выполнение самых важных частей своего доказательства потребуется 5 лет он не
37:16
утверждает что сможет сделать всё за 5 лет но это было бы интересным проектом на самом деле он уже
37:21
в процессе Итак для помощи в моём доказательстве говорим о машинном обучении Итак машинное обучение
Машинное обучение раскрывает тайны теории узлов
37:31
Да это использование нейронных сетей для предсказания ответов на различные вопросы
37:37
которые можно использовать во множестве способов Я думаю что пропущу первый способ о котором я говорил а именно использование нейронных сетей для поиска решений к частным дифференциальным
37:47
уравнениям Что является очень захватывающим новым инструментом в уравнениях в частных производных но
37:54
я пропущу Это я бы а сказал что стоит поговорить о другом применении машинного обучения в теории
38:00
узлов теория узлов – Это довольно интересная область математики это интересная область
38:05
которая объединяет множество различных областей математики и они на самом деле не общаются друг с другом Итак Узел – это просто петля из нити или кривой на самом деле в пространстве которое
38:16
замкнута два узла эквивалентны если существует способ непрерывно деформировать Один узел в
38:22
другой таким образом чтобы нить не пересекала саму себя таким образом основные вопросы в теории узлов
38:29
заключаются в том когда два узла эквивалентны если я дам вам два узла Есть ли способ превратить один
38:35
в другой то обычно вы подходите к этому вопросу разрабатывая так называемые инварианты узлов это
38:41
различные числа Иногда также многочлены которые можно прикрепить к узлу и эти числа не меняются
38:47
независимо от того как вы постоянно деформирует разные инварианты они не могут быть эквивалентными
38:56
Итак существует множество типов узлов множество инвариантов Есть нечто называемое сигнатурок
39:02
бы подсчитывает вы расправляется узел и считаете пересечения Идут ли пересечения сверху или снизу и
39:09
создаёте определённую матрицу и так далее и есть определённое целое число называемая сигнатурок
39:14
что это один тип узлового инварианта существуют известные многочлены называемые многочленом Джонса
39:19
и многочленом хольм которые связаны со многими областями математики Но я не буду об этом говорить а затем есть такие вещи как гиперболические инри которые происходят из геометрии Вы можете
39:29
взять дополнение узла и это на самом деле то что называется это обычно гиперболическое пространство он имеет определённую геометрическую структуру у него есть понятие расстояния и вы
39:41
можете сохранять его как объём и некоторые другие инварианты Итак это инварианты которые являются
39:47
действительными или комплексными числами таким образом каждый узел имеет некоторую комбинатор ную вариацию такую как сигнатуры и это связано с этими геометрическими инвариантами такими как
39:58
гиперболические инварианты Итак вот целый список узлов с различными гиперболические инвариантами
40:04
существует такое понятие как гиперболический объём и гомологическая форма выреза и так далее И это реальные и комплексные числа но никто не знал о какой-либо связи между ними существовали два
40:15
отдельных способа создания статистики узлов и между ними не было связи поэтому только
40:22
совсем недавно люди начали использовать машинное обучение чтобы решить эту проблему они создали
40:27
базы данных миллионов узлов что уже было несколько нетривиальной задачей и обучили нейронную сеть на
40:33
этих данных они обнаружили что после обучения нейронной сети можно было предоставить ей все
40:39
инварианты гиперболической геометрии и в 90% случаев она угадывал правильную сигнатуру Итак
40:45
вы создали эту чёрную коробку и она скажет Вам как подпись была каким-то образом скрыта где-то в этих
40:51
геометрических ин вариантах но она не сказала вам как это была просто чёрная коробка Да так
40:57
Итак это всё ещё полезно потому что как только у вас есть эта чёрная коробка Вы можете просто с ней поиграть следующее что они сделали это на самом деле очень
41:05
простой анализ это то что называется а анализом заметности то есть что делает
41:12
этот чёрный ящик принимает около двадцати различных входных данных для каждого
41:27
из двадцати входных данных которые они нашли только три из них действительно сыграли значительную роль в результате остальные 17 были едва ли релевантны и это были не те три которые
41:37
они ожидали они ожидали что объём например будет очень важен а объём оказывается почти несущественным существовало три нечто называемое продольным преобразованием и действительные и
41:47
комплексные части преобразования Марадоны эти три инварианта были самыми важными Итак Как только они
41:54
определили наиболее важные из них Они могли просто напрямую построить график сигнатуры по отношению
41:59
к этим трём конкретным входным данным а затем они могли оценить ситуацию визуально вместо того чтобы
42:05
использовать нейронную сеть Они использовали человеческую сеть чтобы увидеть О хорошо здесь есть некоторые очевидные паттерны и глядя на эти графики они действительно могли делать
42:15
предположение о том что на самом деле происходит они сделали предположение на основе этого которое оказалось неверным Но на самом деле Они использовали Я думаю что они вернулись к нейронной
42:24
сети Чтобы показать что это было неправильно но затем когда их гипотеза оказалась неверной Они
42:30
смогли её исправить и нашли исправленную версию своей гипотезы которая действительно объясняла это явление и Как только они нашли правильную формулировку им удалось её доказать Таким образом
42:40
у них действительно Есть теоретическое объяснение почему подпись так тесно связано с этими конкретными с этими конкретными статистическими данными Итак я думаю что это способ которым
42:51
машинное обучение всё чаще используется в математике это не решает проблему напрямую но
42:57
даёт вам все эти действительно полезные подсказки о том Каковы связи и куда их искать Но вам всё
43:03
равно нужен человек чтобы на самом деле установить эти связи а затем наконец У нас есть большие
ChatGPT vs IMO: может ли ИИ решать олимпиадные задачи?
43:09
языковые модели которые являются самыми яркими и возможно стали главными новостями знаете нейронные
43:15
сети существуют уже 20 лет языковые модели появились около 5 лет назад но они только недавно
43:22
стали выдавать результаты на уровне человека Так что вы вероятно всё слышали о gpt 4 это текущая
43:29
модель Chat gpt очень известным образом Когда вышел gpt 4 была опубликована статья описывающая
43:36
его возможности и ему в основном задали вопрос из имо 2022 года это немного упрощённая версия Если
43:44
вы изучали 22 амо Это не совсем та же форма Но это упрощённая Форма И для этого конкретного вопроса
43:50
на самом деле вы задаёте вопрос и он действительно даёт полное правильное решение этого вопроса
43:57
на самом деле это решило задачу имо К сожалению это крайне выборочный пример Я думаю что они
44:03
протестировали сотни вопросов уровня imo и по моим оценкам их уровень успеха составил около 1% Так
44:09
что эту конкретную задачу им удалось решить и им пришлось правильно оформить задачу чтобы получить
44:15
решение но всё равно это довольно удивительно С другой стороны забавно что инструменты
44:21
искусственного интеллекта могут легко справляться с теми задачами которые людям даются с трудом В
44:27
то время как с теми Что людям кажутся простыми и часто испытывает трудности это очень ортогональный
44:32
способ решения проблем в очень связанной статье или презентации Они попросили ту же модель
44:38
выполнить базовое арифметическое вычисление 7 x 4 + 8 умножить на 8 и модель которая просто
44:45
угадывает наиболее вероятный результат на основе входных данных в основном угадала что ответ
44:50
120 затем она Остановилась и сказала хорошо возможно мне стоит объяснить почему это 120 Итак они сделали это Шаг за шагом но но когда они делали это Шаг за шагом они на самом деле пришли
45:00
к правильному ответу который равен 92 а не к тому ответу с которого начали Так что если вы Спросите
45:05
Подождите но вы же сказали что это было 120 и они сказали О это была опечатка Извините правильный
45:11
ответ 92 Так что они не решают проблему с помощью первых принципов они просто предполагают на каждом
45:18
этапе вывода Что является самым естественным чтобы сказать следующее и удивительно что иногда это
45:24
срабатывает но часто нет И до сих пор продолжаются работы над тем как сделать это более точным люди
45:33
пробуют всевозможные вещи вы можете подключить эти модели к другому более надежному программному
45:40
обеспечению Итак на самом деле вы увидите презентацию после которой будет подключена большая
45:46
языковая модель Где вы не выполняете вычисления самостоятельно А передаёте их на обработку Python
45:53
в этом случае но ещ одно что вы можете сделать это языковую модель выдавать только правильные
45:59
ответы заставив модель выводить информацию на одном из этих проверяющих языков и если это
46:05
не компилируется вы отправляете это обратно и и и должен попробовать снова или вы можете попробовать
46:12
научить его напрямую тем же методом решения задач которые вы используете для решения задач аймо пробуйте простые примеры доказательства от противного Старайтесь действительно доказать Шаг
46:21
за шагом и так далее люди пробуют всевозможные подходы мы всё ещё далеки от того чтобы
46:27
решить большую часть скажем математических задач Не говоря уже о задачах математических
46:34
исследований но мы движемся вперёд помимо того что я могу непосредственно решать проблемы на
46:42
самом деле это также полезно просто как муза я сам использовал эти модели я экспериментировал
46:50
с различными задачами у меня была проблема с комментированием я ССО но они не сработали Поэтому
46:58
в качестве эксперимента Я просто спросил у gpt какие другие техники вы бы предложили для решения этого вопроса и это дало мне список из дети техник пять из которых я уже пробовал или которые явно не
47:10
были полезны Ну да пара из них не была полезной но была одна техника которую я не пробовал а именно
47:17
использование генерирующих функций для этого конкретного вопроса Как только они это предложили
47:22
Я понял что это правильный подход но я его упустил что как собеседник Это довольно полезно сейчас это
47:31
не отлично но и не совсем бесполезно существует ещё один тип помощи ии который может стать
47:42
очень полезным да для помощи в доказательствах написание формальных доказательств утомительно
47:48
это как придирчивый язык программирования точно соблюдайте синтаксис Если вы пропустите шаг он не
47:56
и я использую один из них называемый github copilot Где вы можете написать половину доказательства и Он попытается угадать что будет следующей строкой и знаете примерно
48:05
в 20% случаев он действительно угадывает что-то близкое к правильному а затем Вы
48:10
можете просто сказать я это приму и сказать хорошо в этом случае я пытался доказать это
48:15
утверждение здесь а серые линии – это те которые предложил койт оказывается первая
48:21
строка бесполезна но вторая строка которую вы не совсем видите на самом деле решила эту конкретну
48:26
проблему вы не можете принять ввод потому что он не обязательно скомпилированный
48:37
они могут автоматически заполнять доказательство если оно состоит из одной или двух строк сейчас
48:47
проводятся эксперименты чтобы как бы итеративности и и предлагающего доказательства а затем вы
48:53
передаёте это обратно компилятор и если проходит с ошибкой вы отправляете сообщение об ошибке
48:59
Обратно мы начинаем с сортов доказательства которые состоят из четыр или пяти строк могут быть ограничены этим методом Так что вы знаете конечно большое доказательство это десятки тысяч
49:09
строк таким образом это ещё не тот момент когда вы можете мгновенно формализовать своё доказательство
Будущее математики: как ИИ изменит исследования
49:15
но это уже полезный разговор хорошо Где мы сейчас есть люди которые надеются что Через
49:22
несколько лет мы сможем использовать компьютеры для непосредственного решения тических задач
49:28
Я думаю что мы ВС ещё далеки от этого для очень узко сфокусированный специализированные и и для
49:35
обработки лишь очень узкого диапазона проблем но даже в этом случае они не являются полностью
49:41
надёжными они могут быть полезными но всё же по крайней мере в течение следующих нескольких
49:48
лет они в основном будут действительно полезной помощью И помимо грубой вычислительной помощи с
49:55
кой знакомы люди пробуют всевозможные креативные вещи я думаю что одно направление которое мне
50:03
кажется особенно захватывающим и которая ещё не стало успешным это то что надеюсь ии стал очень
50:10
хорош в генерации хороших гипотез Итак мы уже видели небольшой пример этого с узлами где они
50:17
уже могли как бы предположить связи между двумя различными статистика Так что вы знаете и есть
50:24
надежда что вы сделаете эти огромные наборы данных и введёте их в ии и он автоматически
50:29
создаст множество хороших связей между различными математическими объектами на самом деле мы ещё не
50:36
знаем как это сделать отчасти потому что у нас нет этих огромных наборов данных но я думаю что это в
50:43
конечном итоге станет возможным меня также радует то что это тип математики который просто ещё не
50:50
существует прямо сейчас поскольку доказательство теорем является таким болезненным и кропотливый
50:55
процессом мы показываем одну теорему за раз или может быть две или три Если вы эффективны но с ии
51:02
Вы можете представить что в будущем вместо того чтобы пытаться решить одну проблему или что-то в этом роде вы берёте класс из 1.000 похожих проблем и вы говорите Хорошо я собираюсь сказать вашему ии
51:12
Попробуй решить эти 1.000 проблем с этой техникой там и он ответит О я могу решить 35% этих проблем
51:19
с этой техникой А что насчёт этой техники Тогда я могу решить этот процент проблем или если я их
51:26
начать исследовать пространство проблем а не просто Каждую из них отдельно и это то что вы либо не можете сделать прямо сейчас либо делаете в течение десятилетий с десятками и
51:36
десятками статей медленно разбираясь в том что вы можете и не можете сделать с различными техниками
51:41
но с этими инструментами Вы действительно могли бы я имею в виду вы могли бы начать заниматься
51:47
математикой в масштабе который действительно не имеет прецедентов Так что я думаю будущее
51:55
будет действительно захватывающим Я имею в виду что мы всё равно будем доказывать теоремы старомодный способом на самом деле нам придётся это сделать потому что мы не
52:03
сможем мы не сможем управлять этими ии если сами не научимся делать эти вещи но мы сможем
52:09
делать много вещей которые сейчас не можем хорошо думаю я на этом остановлюсь Спасибо
52:15
большое Есть вопрос
Вопросы и ответы с профессором Тао
52:30
Итак у нас плотный график но мне сказали что у нас есть время на три
52:36
вопроса или около того Так что если люди поднимут руки кто-то
52:42
там Спасибо Вы меня слышите Спасибо это была прекрасная речь мне особенно понравилось говорить
52:55
о формализации математики Но одна вещь которую вы не упомянули – это велоблогер геометрию потому что
53:05
совершил ошибку и начал формализовать теорию типов гомо топи Мне было бы интересно узнать изучали ли
53:13
вы это и есть ли у вас какие-либо комментарии по этому поводу правильно Да что касается форте Ута
53:19
Да он Беспокоился о кризисе в некоторых областях математики включая некоторые которые он создал что
53:26
Да доказательства были настолько абстрактными и сложными что не было возможности проверить что они
53:32
полностью верны да Он предложил изменить основу математики на теорию типов более высокого порядка
53:38
теорию типов гомо топи которая более надёжно Если вы Измените основную аксиому математики многое из
53:46
того что вы доказываете в этой теории всё равно останется верным существует языки для помощников
53:51
по доказательствам которые основаны на этом виде теории типов гомо той Лин на самом был ратан с
53:57
этой целью потому что Лин хочет формализовать много традиционной математики которая не написана
54:04
на этом языке Я надеюсь что в будущем будет несколько помощников по доказательствам есть
54:09
языки для помощников с разными плюсами и минусами одной из вещей который у нас сейчас нет является
54:14
автоматический способ перевода доказательства с одного языка на другой на самом деле это одно из
54:20
мест где и я думаю будет очень полезен как только мы это получим Если у вас есть друя вашей основы
54:27
математики мы могли бы надеюсь Просто перевести доказательство которое было формализована на
54:33
одном языке на другой И тогда все будут убеждены включая вела Бродского если бы он всё ещё был
54:38
жив Надеюсь Э да да я имею в виду что Существует несколько подходов к формализации математики и нам
54:47
не следует определённо не следует зацикливаться на каком-то одном конкретном стандарте прямо сейчас
54:57
а ну я м
55:06
хорошо это случайный процесс Ну ладно Ну это не будет совсем актуально для темы доклада но
55:16
Недавно я подавал заявки на аспирантуру и совет который мне дали профессора сводился к тому что
55:23
чем длиннее тем лучше кажется существует общее Согласие в том что математикам необходима как
55:30
мне кажется вырасти до Больших идей м некоторые с этой точки зрения Как вы оцениваете своё решение
55:40
поступить в университет в таком молодом возрасте как это повлияло на вас как на математика Я как на
55:48
человека Ну у меня были очень хорошие наставники Как в школе так и на уровне бакалавриата и
55:59
магистратуры Я имею в виду что это не гонка вы поступаете в университет когда готовы не стоит
56:08
уходить только потому что вам сказали что для этого нужно X лет или что-то в этом роде Я не знаю что на это сказать Я думаю что для разных людей это по-разному это было очень важно для
56:19
меня Я поступил в университет Когда мне было 13 лет но в университет который находился очень
56:25
близко к тому месту где я жил поэтому я жил с родителями и они на самом деле довольно много
56:31
возили меня в университет на все мои занятия Если бы у меня этого не было я не думаю что у меня был
56:36
бы хороший опыт Так что это действительно зависит Я поступил в университет в очень молодом возрасте
56:43
это не значит что все должны это делать да на этот вопрос нет единственного ответа спасибо
56:56
хорошо Итак ещё один более общий вопрос учитывая что вы внесли вклад в Поистине
57:16
миллион математических областей Как вы выбираете свою следующую тему исследования
57:23
и проблему которую хотите решить и также каков ваш число рдш хорошо что ж мой номер ёша равен
57:30
двум это просто но м на самом деле я не знаю я имею в виду в начале своей карьеры у меня
57:36
были наставники которые предлагали мне задачи в наши дни это часто происходит просто случайно Я
57:42
имею в виду что Математика – это очень социальная деятельность вы посещаете множество мероприятий Я
57:48
имею в виду что после этого я собираюсь на математическую конференцию в Эдинбурге и я
57:54
собираюсь поговорить с множеством людей в точной области связанной с этой гипотезой pfr на самом
58:01
деле у меня будут математические беседы из этого возникнут некоторые исследовательские вопросы у
58:07
меня есть несколько долгосрочных проектов которые я хотел бы решить но всё чаще я
58:13
замечаю что это вопросы которые возникают в ходе беседы с другими математиками Да Вы знаете я не
58:21
знал что буду говорить так много о и например 2 лет назад Да я думаю что Людям нужно будет
58:30
быть более гибкими в будущем всё ещё будут люди которые будут специализироваться на одной теме
58:38
и просто захотят стать мировыми экспертами в и но по моему мнению всё больше людей со временем будут
58:44
перемещаться между темами они будут находить интересную новую математику каждые несколько лет просто общаясь с другими людьми хорошо Я думаю нам действительно нужно двигаться дальше следующий
58:56
Самон кол из xtx который расскажет о олимпиаде по математике с использованием и [аплодисменты]