← All repos

LeanSearchClient

Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)

GitHub
Browse cluster: Lean4 Formal Verification & Cryptography →
69commits
8contributors
1languages

Tech stack & purpose

LeanSearchClient provides syntax for searching within the Lean proof assistant using natural language queries against multiple backend services, including leansearch.net, LeanStateSearch, and Loogle. The tool enables users to search for Lean tactics and theorems through four syntactic forms—as commands, terms, tactics, or state-based queries—with results displayed in the Lean Infoview and selectable via clickable suggestions. The project is built for Lean and integrates with external search APIs to help developers discover relevant library functions and proof strategies during interactive development.

Languages

Lean
100.0%

Contributors