Lean
Язык программирования и система интерактивного доказательства теорем, в которой каждый логический шаг проверяется компьютером. Применяется для формализации математики (в том числе в библиотеке mathlib) и для проверки доказательств, полученных людьми или моделями ИИ; корректность вывода гарантируется только при верно записанной формулировке.
проверено по: lean-lang.org ↗
См. также
- MathlibОткрытая библиотека формализованной математики для системы доказательства теорем Lean, которую развивает сообщество. Все определения и теоремы в ней проверены компьютером. Библиотеку используют математики, преподаватели и разработчики ИИ, которые учат модели доказывать теоремы.
- Formal ConjecturesОткрытый репозиторий Google DeepMind с математическими гипотезами и нерешёнными задачами (например, проблемами Эрдёша), формально записанными на языке Lean 4 с библиотекой Mathlib. Обычно в нём лежат только точные формулировки, без доказательств. Коллекция служит бенчмарком для систем автоматического доказательства теорем и автоматической формализации: предложенное решение проверяет Lean, а не человек.
В новостях
Meta даст пяти университетам США свои модели и 2 млн долларов на науку
Язык программирования и система для доказательства теорем: утверждение и доказательство записывают так, что компьютер проверяет каждый шаг.
OpenAI заявила, что её ИИ опроверг гипотезу об экспоненциальном времени решения трудных задач
Язык программирования и система для формальной записи математических доказательств: компьютер проверяет каждый шаг. Проверка подтверждает доказательство того утверждения, которое записали формально, а совпадает ли оно с исходной задачей, решают люди.
Claude Mythos 5 придумала квантовые схемы экономнее лучших опубликованных
Язык программирования и система для компьютерной проверки математических доказательств: программа проверяет каждый шаг рассуждения и не пропускает пробелов.
Google показала научные результаты модели Gemini 4 Argon и даст 10 000 учёным бесплатный доступ
Язык программирования и система, где математические доказательства записывают так, что их правильность проверяет компьютер.
Андрей Карпаты считает, что 6 млрд человек почти не сталкивались с ИИ. Что говорят данные
Язык программирования и система для доказательства теорем: математическое доказательство записывают на нём так, что его правильность проверяет компьютер.
Код для компьютерной проверки доказательства OpenAI о Навье — Стоксе расходится со статьёй
Язык программирования и система для записи математических доказательств: компьютер проверяет каждый логический шаг и принимает доказательство, только если в нём нет пропусков.
Meta дала агенту Muse почту и управление Mac, а модель только пообещала
Язык программирования и система для записи математических доказательств, которые компьютер проверяет сам. Верно ли доказательство, решает её ядро — небольшая программа-проверяльщик.
Профессор NYU обвинил OpenAI в перехвате задачи Навье — Стокса. Что ответили в компании
Язык программирования и система автоматической проверки доказательств. Если доказательство записано на Lean и прошло проверку, каждый его шаг проверен машиной.
OpenAI заявила, что ИИ решил задачу тысячелетия об уравнениях Навье — Стокса
Язык программирования и система проверки доказательств. Каждый шаг доказательства на Lean проверяет компьютер, поэтому такое доказательство надёжнее текста, который читает человек. Остаётся одно условие: формулировка теоремы должна быть записана верно.