This was posted a while back on the Lean Zulip: LeanDojo LeanDojo: Theorem Proving with Retrieval-Augmented Language Models According to their description, LeanDojo is an open-source Lean play . . . Read more

An improved search engine for Lean: https://loogle.lean-fro.org/ https://github.com/nomeata/loogle I haven’t used it yet but it looks promising. I personally don&rs . . . Read more