工具汇集
搜索：
LeanSearch，支持自然语言搜索， 自带语义增强功能
LeanExplore，支持自然语言搜索
Moogle，版本较老
Loogle!，支持按表达式和字符串搜索
Lean State Search，支持根据状态搜索，必须包含⊢
编译：
官方playground 在线编译器，仅支持最新分支和最新发行版
ReasLab IDE，同时提供了很多Lean教程的模版
证明：
Kimina Prover Demo，用于调用模型解决lean证明，支持自然语言输入，先将问题转换为lean形式化描述再做证明，可以同时做16种尝试
大语言模型：
Google AI Studio，可以使用Gemini 2.5 Pro，相比直接的Gemini网页调整功能更多