LeanLLM nabízí jednotné rozhraní pro práci s jazykovými modely v programovacím jazyce Lean 4. Nová knihovna spojuje přímá API poskytovatelů, cloudové služby a lokální servery kompatibilní s OpenAI. Dokumentace uvádí podporu modelů Anthropic, OpenAI, Google Gemini, DeepSeek, Qwen a Mistral, ale také služby OpenRouter, AWS Bedrock či Azure OpenAI. Vývojář může změnit poskytovatele v konfiguraci bez přepisování kódu, který odesílá požadavky. Příklady ukazují jednoduché dotazy, vícekolovou konverzaci, průběžné přijímání odpovědi i práci s voláním nástrojů. Knihovna vyžaduje Lean 4.34.1 a libcurl; instalace odkazuje na verzi 0.1.0. Jde o klientskou vývojářskou vrstvu, nikoli nový jazykový model nebo automatickou záruku správnosti formálních důkazů.

Radyz

Radyz publikuje komentáře a praktické texty o AI nástrojích, ChatGPT, Claude a dění kolem OpenAI a Anthropicu. Na webu se soustředí na srozumitelný výklad, vlastní zkušenost a důraz na to, co je pro čtenáře skutečně užitečné.