LeanDojo Benchmark 4

<p>Lean 4 version of the dataset in the paper:</p> <p><a href="https://leandojo.org/">LeanDojo: Theorem Proving with Retrieval-Augmented Language Models</a><br> <a href="https://yangky11.github.io/">Kaiyu Yang</a>,&nbsp;<a href="https://aidanswope.com/about">Aidan Swope</a>,&nbsp;<a href="https://minimario.github.io/">Alex Gu</a>,&nbsp;<a href="https://www.linkedin.com/in/rchalamala">Rahul Chalamala</a>,&nbsp;<a href="https://www.linkedin.com/in/peiyang-song-3279b3251/">Peiyang Song</a>,&nbsp;<a href="https://billysx.github.io/">Shixing Yu</a>,&nbsp;<a href="https://www.linkedin.com/in/saad-godil-9728353/">Saad Godil</a>,&nbsp;<a href="https://www.linkedin.com/in/ryan-prenger-18797ba1/">Ryan Prenger</a>,&nbsp;<a href="http://tensorlab.cms.caltech.edu/users/anima/">Anima Anandkumar</a></p>