On: LeanDojo: Theorem Proving in Lean Using LLMs

[dkga]

Perhaps a simpler and more reachable approach at this point would be to use the mathlib documentation to fuel a RAG on top of the fine-tuned/specialised model.