Словарь
Formal Conjectures
Открытый репозиторий Google DeepMind с математическими гипотезами и нерешёнными задачами (например, проблемами Эрдёша), формально записанными на языке Lean 4 с библиотекой Mathlib. Обычно в нём лежат только точные формулировки, без доказательств. Коллекция служит бенчмарком для систем автоматического доказательства теорем и автоматической формализации: предложенное решение проверяет Lean, а не человек.