Язык программирования, который судит математику — Лео де Моура

Леонардо де Моура создал Lean и участвовал в создании Z3. -- Этот эпизод спонсируется компанией Parallel. Parallel, где агенты находят ответы: веб-поиск, извлечение данных и API для глубоких исследований, созданные для агентов ИИ. Начните бесплатно с сервером Parallel MCP и 5 долларов кредитов каждый месяц: https://parallel.ai/mlst?utm_source=c... --- Тим Скарф обсуждает с Лео, как Lean вышел за рамки своей первоначальной аудитории, почему зависимые типы и Mathlib сделали его полезным для работающих математиков, и что происходит, когда формальная верификация покидает лабораторию. Де Моура объясняет принцип работы небольшого доверенного ядра и независимых проверяющих, а также рассказывает о недавнем инциденте с Коллатцем, когда предполагаемое доказательство было принято как официальным ядром Lean, так и Nanoda, по-видимому, путем использования разных ошибок в каждом из них. Затем разговор переходит к доказательствам и программному обеспечению, созданным ИИ. Агенты Клода перестраивают zlib в Lean, и результат подтверждается, однако пример выявляет лазейку в центре шоу: доказательство подтверждает только ту спецификацию, которую выбрали люди для написания. Де Моура описывает поиск доказательств как игру, отделяет формальную компетентность от математического понимания и задается вопросом, что означает авторство, когда модели могут генерировать доказательства в больших масштабах. В заключительном аргументе ответственность человека ставится на первое место: выбор определений, оценка абстракций, курирование Mathlib, проверка сертификатов и решение, какие проблемы заслуживают внимания. Он также размышляет о будущем Lean после его основателя и предлагает практическую отправную точку для новых пользователей. -- ВРЕМЕННЫЕ МЕТКИ: 00:00:00 Вступление: зеленая галочка может лгать 00:00:59 Собор или базар: кто контролирует ядро ​​Lean? 00:04:55 Почему ядро ​​Lean остается небольшим и защищенным 00:08:07 Очистка Slack, закон Брандолини и Lean FRO 00:11:12 Эксплойт Коллатца: два ядра, две ошибки 00:16:44 Больше ядер, взлом вознаграждений и безопасность за счет прозрачности 00:21:04 Спонсор: Parallel 00:21:59 Ким Моррисон, Клод и доказательство zlib 00:25:25 Можем ли мы специфицировать сложные системы? 00:28:04 Изменение спецификаций: доказательства дешевле переделывать с помощью ИИ 00:31:27 От Lean 1 к Lean 4 00:34:57 Зависимые типы простыми словами 00:37:25 Расширяемость Lean 4 и рост Mathlib 00:41:44 Mathlib как инфраструктура: формальные границы 00:44:15 Креативность, абстракция и поиск орехов 00:48:46 Хлебные крошки, а не обучение: чего не хватает агентам ИИ 00:53:03 Компетентность без понимания и проверенные ограничители 00:56:21 Человек по-прежнему является автором? 01:01:44 AlphaProof, LLM и почему сертификаты по-прежнему важны 01:06:38 Что ждет Lean в будущем и каково его наследие 01:11:42 Как начать изучать Lean --- ССЫЛКИ: инструмент: [00:00:48] Lean https://lean-lang.org/ [00:01:24] Mathlib https://github.com/leanprover-communi... [00:12:09] nanoda_lib https://github.com/ammkrn/nanoda_lib [00:12:19] CollatzLean https://github.com/xrchz/CollatzLean/... [00:13:06] Проблема Lean 14576 https://github.com/leanprover/lean4/i... [00:13:21] Запрос на слияние Lean 14577 https://github.com/leanprover/lean4/p... [00:13:45] Запрос на слияние nanoda_lib 22 https://github.com/ammkrn/nanoda_lib/... [00:15:33] Lean компаратор https://github.com/leanprover/comparator [00:18:02] Lean4Lean https://github.com/digama0/lean4lean [00:19:50] ARC-AGI-3 https://arcprize.org/arc-agi/3 [00:21:59] lean-zip https://github.com/kim-em/lean-zip [00:29:45] CompCert https://compcert.org/ [00:29:45] seL4 https://www.sel4.org/ [00:30:23] Z3 https://github.com/Z3Prover/z3 [00:38:10] Veil https://github.com/verse-lab/veil [00:38:10] Velvet https://github.com/verse-lab/velvet организация: [00:00:52] Lean FRO https://lean-lang.org/fro/ [00:42:39] Mathlib Initiative https://mathlib-initiative.org/about/ [01:11:42] Computerphile    / @computerphile   персонаж: [00:05:11] Илья Сергей https://ilyasergey.net/ [00:10:31] Йоахим Брайтнер https://www.joachim-breitner.de/ [00:32:58] Адам Члипала https://adam.chlipala.net/ [00:38:42] Кевин Баззард https://www.ma.imperial.ac.uk/~buzzard/ [01:10:16] Теренс Тао https://terrytao.wordpress.com/ книга: [00:08:19] Доказательство в коде https://us.macmillan.com/books/978037... другое: [00:10:05] Закон Брандолини https://en.wikipedia.org/wiki/Brandol... [00:45:33] Новый результат о единичных расстояниях https://openai.com/index/model-dispro... [01:01:08] Великая теорема Ферма формализация https://imperialcollegelondon.github.... статья: [00:34:36] Доказатель теорем Lean 4 и язык программирования https://doi.org/10.1007/978-3-030-798... [01:02:06] AlphaProof https://doi.org/10.1038/s41586-025-09... [01:04:24] ...