LeanLLM — библиотека для приложений на Lean 4, которая, согласно README проекта, предоставляет единый типизированный интерфейс к моделям и способам подключения разных поставщиков. В описании указана версия v0.2.0; дата её выпуска не установлена. Для разработчика это набор примеров вызова модели, диалога, потоковой выдачи и инструмента в одном SDK. README LeanLLM с примерами и требованиями.
Модели и подключения
README перечисляет Anthropic Claude, OpenAI, Google Gemini, DeepSeek, Kimi/Moonshot, Z.AI GLM, Qwen, MiniMax, xAI Grok и Mistral. Среди способов подключения названы API поставщиков, OpenRouter, AWS Bedrock, Azure OpenAI, Google Vertex AI, некоторые OAuth-сессии и локальные OpenAI-совместимые серверы. Это заявленный перечень проекта, а не результат проверки совместимости каждой модели.
Запросы, диалоги и потоковая выдача
Для одиночного вопроса пример использует ask. Для диалога completion принимает список сообщений; README указывает, что ответ содержит текст ассистента, причину остановки и сведения об использовании токенов. Для получения текста частями показаны askStream и completionStream — последний вариант предназначен для диалоговой истории.
Локальный сервер и инструменты
В конфигурации ModelConfig можно задать модель и провайдера. В качестве примера локального подключения README приводит совместимый с OpenAI адрес http://localhost:11434/v1 и пользовательское имя модели; в описании этого сценария сказано, что ключ API не требуется. Адрес дан как пример, а не как универсальная настройка для всех локальных серверов.
Для инструментов README показывает объявление через ToolSpec и чтение вызовов из resp.toolCalls. Пример выводит имя инструмента и его аргументы; он сам по себе не показывает автоматическое выполнение этих вызовов приложением.
Установка и ограничения
Для подключения библиотеки README предлагает добавить зависимость в lakefile.toml с ревизией v0.2.0. Указаны требования Lean v4.34.1 и libcurl во время выполнения. Для облачных подключений нужны соответствующие переменные окружения с ключами; для OpenRouter приведена OPENROUTER_API_KEY. В примере пользовательского совместимого адреса указаны LLM_API_KEY и необязательная OPENAI_API_KEY. Дата публикации README и дата выпуска не установлены. Работоспособность примеров независимо не подтверждена, поэтому перечисленные интеграции и сценарии следует считать описанием проекта, а не результатами тестирования.
