Comment by rprenger

You can have both! LeanDojo: Theorem Proving with Retrieval-Augmented Language Models https://arxiv.org/abs/2306.15626 (shameless plug)