Mathlib
Открытая библиотека формализованной математики для системы доказательства теорем Lean, которую развивает сообщество. Все определения и теоремы в ней проверены компьютером. Библиотеку используют математики, преподаватели и разработчики ИИ, которые учат модели доказывать теоремы.
проверено по: github.com ↗
См. также
- LeanЯзык программирования и система интерактивного доказательства теорем, в которой каждый логический шаг проверяется компьютером. Применяется для формализации математики (в том числе в библиотеке mathlib) и для проверки доказательств, полученных людьми или моделями ИИ; корректность вывода гарантируется только при верно записанной формулировке.
- Formal ConjecturesОткрытый репозиторий Google DeepMind с математическими гипотезами и нерешёнными задачами (например, проблемами Эрдёша), формально записанными на языке Lean 4 с библиотекой Mathlib. Обычно в нём лежат только точные формулировки, без доказательств. Коллекция служит бенчмарком для систем автоматического доказательства теорем и автоматической формализации: предложенное решение проверяет Lean, а не человек.
В новостях
Hugging Face превратила 369 теорем OpenAI в задачи для обучения моделей
Открытая библиотека формализованной математики для Lean, которую пишет сообщество: в ней собраны определения и уже доказанные теоремы.