Impact of additional_imports on MiniF2F

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.