Lean 4 — это современная интерактивная среда для формальной верификации и доказательства теорем, набирающая популярность в среде математиков, программистов и исследователей, занимающихся формализацией доказательств. При работе с Lean 4 огромную роль играет возможность быстрого и точного поиска нужных теорем в обширной библиотеке Mathlib и пользовательских проектах. В силу специфики языка и среды поиск тут выходит далеко за рамки обычного текстового поиска и требует использования как формальных так и семантических методов. В этом обзоре мы рассмотрим основные типы поисковых систем для Lean 4, особенности каждой из них, а также дадим практические рекомендации по их эффективному применению. В Lean существуют две основные категории поисковых систем — нейронные (векторные) и формальные.
Нейронные поисковики, такие как Moogle, LeanSearch, LeanExplore и Search-Mathlib, работают на основе больших языковых моделей и техники векторного представления теорем. Каждая теорема в Mathlib кодируется в виде эмбеддинга — многомерного числового вектора, отражающего смысл формулы. Поисковый запрос тоже превращается в эмбеддинг, а затем с помощью косинусного сходства или аналогичного критерия находятся наиболее близкие к запросу теоремы. Это позволяет искать по естественному языку, частичным описаниям, приближённым формулам или даже неполным фразам без необходимости точного знания синтаксиса Lean. Такой подход очень удобен на первоначальных этапах формализации, когда пользователь ещё не уверен, как именно сформулирована нужная ему теорема в Mathlib, или не хочет тратить время на написание точного Lean-терма.
Семантический поиск по своей сути более гибкий, более снисходительный к синтаксическим ошибкам и отражает смысл, а не точные конструкции. Это делает его незаменимым помощником при исследовании математической библиотеки и поиске аналогий. В свою очередь формальные поисковые системы, например Loogle и тактики exact?, работают по-другому. Вместо обработки смысла они ищут точные совпадения по формальному описанию теоремы. Такие поиски требуют, чтобы пользователь хорошо представлял собой форму искомого утверждения и умел формировать запросы на языке Lean с нужными символами и структурами.
Преимущество формальных поисков в том, что они возвращают гарантированно все подходящие теоремы из Mathlib и локальных контекстов, если запрос составлен корректно. Это полезно при точном кодировании доказательства и оптимизации работы с уже формализованными сведениями. Одним из самых популярных семантических поисковых движков является Moogle, разработанный Morph Labs. Он стал пионером в области семантического поиска теорем и долгое время возглавлял рейтинг подобных сервисов. Moogle позволяет вводить любые запросы — от LaTeX-формул и фрагментов кода до естественного языка.
Тем не менее, обновления этого инструмента замедлились, и сообщество Lean все активнее обращается к альтернативным сервисам. LeanSearch — современный конкурент Moogle, поддерживаемый командой AI4Math из Пекинского университета. Этот движок открыто разработан, известна подробная архитектура и особенности его работы. LeanSearch не просто переводит формальные заявления в векторы, а строит развернутую неформализацию, включая название теоремы, её тело, инфологирование соседних утверждений и документацию. Такой комплексный подход позволяет поиску давать более релевантные результаты и чаще выводить нужные теоремы в верхнюю часть списка.
Уникальной функцией LeanSearch является возможность автоматической генерации естественно-языкового описания запроса с помощью GPT-4, что помогает пользователям улучшить точность поиска без глубоких знаний синтаксиса Lean. Новый инструмент LeanExplore вышел с акцентом на индексирование не только теорем, но и метапрограммирования в Lean и Mathlib. Это расширяет область применения поиска, позволяя не только находить доказательства, но и вспомогательные функции и конструкции, востребованные при разработке тактик и самого кода на Lean. Search-Mathlib — небольшой учебный проект, но продемонстрировавший, что даже с минимальными ресурсами можно создать работоспособный семантический поисковик. Тем не менее, для серьёзного использования чаще выбирают LeanSearch и Moogle.
Сформальный поиск в Lean реализован в виде Loogle и тактики exact?. Loogle вырос из команды Mathlib и служит мощным инструментом для поиска теорем по их формальным описаниям с использованием унифицированных шаблонов и «дырок» (?_) для неизвестных подвыражений. Он позволяет пользователям создавать заявки со значительной свободы и получать полные списки всех теорем, соответствующих шаблону. Однако Loogle ориентирован на Mathlib и не индексирует локальные определения из проекта. Тактика exact? (бывшая library_search) и её родственники apply? и rw? позволяют искать и применять правильные вспомогательные теоремы для закрытия текущей цели доказательства прямо в процессе построения доказательства.
exact? особенно полезна для нахождения точного одношагового применения, закрывающего цель, если необходимые гипотезы уже доступны. Это одна из самых активно используемых техник для быстрой формализации конкретных целей, но она ограничена по глубине поиска и требует адекватного контекста. Помимо специализированных поисковых систем, существуют инструменты LeanCopilot и LeanStateSearch, которые используют машинное обучение для рекомендаций следующий шагов доказательства, подбирая релевантные теоремы согласно текущему состоянию. Они представляют собой более интеллектуальные помощники, но пока менее популярны и требуют дополнительного освоения. Для многих пользователей незаменимой оказывается простая команда CMD+F в редакторе — классический поиск по тексту файлов.
В небольших проектах такой метод порой оказывается самым быстрым и очевидным способом найти нужную теорему или определение. Более того, при отсутствии поддержки персонального семантического поиска по проектам, такой ручной обход часто является единственным вариантом. Интересным направлением является использование больших языковых моделей (LLM), таких как Claude, для создания ad-hoc семантических поисков по локальным проектам. Копирование в модель текста с только заявленными теоремами без тел доказательств позволяет настроить собственную базу знаний проекта с возможностью естественно-языковых запросов и получения подсказок. Хотя данный подход требует дополнительных затрат и навыков, он даёт мощный инструмент для локального поиска в Lean.
На практике рекомендуется комбинировать разные подходы: сначала использовать нейронные поисковики для общего понимания, подбора кандидатов, потом уточнять запрос в формальных системах, а при необходимости применять тактики exact? для быстрого закрытия целей. В дополнение к этому, привычка умело рефакторить поисковые формулировки и уметь абстрагировать суть задачи значительно повышает продуктивность. Поисковая культура в Lean 4 — это не только про инструменты, но и про подход к формализации: умение выражать свою проблему в понятных серверам форматах, осознавать важность контекста и поиска взаимосвязей. С развитием технологий и сообществ мы можем ожидать дальнейшего улучшения качества поисковых систем, интеграции локального индексирования и более удобных интерфейсов на базе ИИ. В целом, эффективный поиск теорем в Lean 4 — это баланс между гибкостью семантических инструментов и точностью формальных методов.
Владение современными поисковыми сервисами и грамотный стиль формулировки запросов существенно ускорят процесс доказательства и позволят пользователям быстрее находить необходимые знания в богатой экосистеме Lean.
