alt Hacker NewsProofSouq.com! https://proofsouq.com
8M+ search index entries over Lean and Rocq corpora and growing; propositions only for now, so more oriented towards premise retrieval at the moment.
ProofSouq.com! https://proofsouq.com
8M+ search index entries over Lean and Rocq corpora and growing; propositions only for now, so more oriented towards premise retrieval at the moment.
Lean also has https://www.leanexplore.com and https://loogle.lean-lang.org/