LeanSearch 用于在 Lean 4 的数学库 Mathlib4 中查找定理。其“查询增强”功能（即网站上的“Augmentation Query”按钮）利用大型语言模型（如 GPT-4 或 DeepSeek-V2-Chat）处理用户输入。
以查询“从 x ≤ y，推导 ball c x ⊆ ball c y”为例，点击“查询增强”按钮后，系统可能生成：“球的单调性：在一个度量空间中，若球心为 c 的球的半径从 x 增加到 y，且 x ≤ y，则半径为 x 的球完全包含在半径为 y 的球内。”这一增强后的描述随后用于搜索，匹配更精确的定理。lakesare.brick.do/how-to-search-for-theorems- … -lean-4-WXebAQkXVmx1
