LeanDojo is a Python library for learning-based theorem provers in Lean, enabling data extraction...