Lean 4
Lean 4 — версия языка функционального программирования и системы интерактивного доказательства теорем Lean с открытым исходным кодом. Математики и разработчики используют её для формализации математики и проверки корректности программ. Построенные формальные доказательства автоматически проверяет небольшое логическое ядро системы.
проверено по: lean-lang.org ↗
См. также
- LeanЯзык программирования и система интерактивного доказательства теорем, в которой каждый логический шаг проверяется компьютером. Применяется для формализации математики (в том числе в библиотеке mathlib) и для проверки доказательств, полученных людьми или моделями ИИ; корректность вывода гарантируется только при верно записанной формулировке.
- MathlibОткрытая библиотека формализованной математики для системы доказательства теорем Lean, которую развивает сообщество. Все определения и теоремы в ней проверены компьютером. Библиотеку используют математики, преподаватели и разработчики ИИ, которые учат модели доказывать теоремы.
- RocqСистема интерактивного доказательства теорем (proof assistant), раньше называлась Coq. В ней записывают математические доказательства и формальные спецификации программ, а система сама проверяет каждый шаг; из проверенных спецификаций можно автоматически получить рабочий код на OCaml или Haskell. С её помощью сделаны, например, проверенный компилятор языка C CompCert и формальное доказательство теоремы о четырёх красках. Близкий аналог — Lean.
- Formal ConjecturesОткрытый репозиторий Google DeepMind с математическими гипотезами и нерешёнными задачами (например, проблемами Эрдёша), формально записанными на языке Lean 4 с библиотекой Mathlib. Обычно в нём лежат только точные формулировки, без доказательств. Коллекция служит бенчмарком для систем автоматического доказательства теорем и автоматической формализации: предложенное решение проверяет Lean, а не человек.
В новостях
Amazon с помощью ИИ доказала надёжность протокола базы данных Aurora
Язык программирования с открытым кодом и средство доказательства теорем. Программа сама проверяет каждый шаг доказательства, поэтому результат можно принять, кто бы его ни написал: человек или модель.