search

lean-dojo / ReProver

Retrieval-Augmented Theorem Provers for Lean
https://leandojo.org
MIT License
208 stars 44 forks source link

Jointly sort theorems and positions in `evaluate.py` #49

Closed matt-seb-ho closed 4 months ago

matt-seb-ho commented 5 months ago

I noticed that in prover/evaluate.py:_get_theorems_from_files, only theorems are sorted. I could definitely be wrong, but my understanding is that theorems and positions are constructed as parallel lists from the .json file and should be kept parallel as the later call to search_unordered zips them together.

I definitely mean for this to be a helpful fix, but if I misunderstood something, please let me know!

Thanks as always for open sourcing LeanDojo and related experiments!

yangky11 commented 4 months ago

Indeed! Thx