InternLM / InternLM/InternLM-Math
Impact of additional_imports on MiniF2F
Open
- Dominant language
- Python
- Stars
- 550
- Forks
- 39
- PR merge metrics
- No merged PRs in 30d
Description
I have a few questions regarding the 'additional_imports' argument. I noticed that the BFS prover sets additional_imports=['Mathlib.Tactics']. Could you please clarify if this has any positive impact on proving minif2f? I did not find any usage of it in Reprover (https://github.com/lean-dojo/ReProver). If additional_imports=[] is set, are there certain math problems in minif2f that cannot be proven? If so, why? Thank you very much for your assistance.
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.