Is it possible to use BM25 with Lean4?

[jogobeny]

Hi,

is it possible to use BM25 with Lean4? I am trying the provided example script from README, but getting this error:

Traceback (most recent call last):
  File "/home/.../Documents/itp-interface/src/test/my_test.py", line 48, in <module>
    state, _, next_state, _, done, info = env.step(action)
                                          ^^^^^^^^^^^^^^^^
  File "/home/.../Documents/itp-interface/src/itp_interface/rl/simple_proof_env.py", line 221, in step
    state_before = self.state
                   ^^^^^^^^^^
  File "/home/.../Documents/itp-interface/src/itp_interface/rl/simple_proof_env.py", line 142, in state
    proof_state, _, _, _ = self._get_current_dfns_thms(ProofEnvInfo(progress=ProgressState.STARTING))
                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/.../Documents/itp-interface/src/itp_interface/rl/simple_proof_env.py", line 464, in _get_current_dfns_thms
    relevant_defns_thms = self._dynamic_proof_executor.get_all_relevant_defns_and_thms(should_print_symbol, only_local, only_proof_state)
                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
AttributeError: 'DynamicProofExecutor' object has no attribute 'get_all_relevant_defns_and_thms'

where DynamicProofExecutor is itp_interface.tools.dynamic_lean4_proof_exec.DynamicProofExecutor.

I have noticed that itp_interface.tools.dynamic_lean_proof_exec.DynamicProofExecutor (Lean 3) has implemented those methods. Is it still possible to use Lean 3 with the current version of itp-interface.

[amit9oct]

Yes it is possible, however, I don't have the bandwidth to implement the search for Lean 4 right away

[amit9oct]

As you mentioned, it can be done by simply implementing those methods for Lean 4. The original paper was written for Lean 3, where all our retrieval experiments were done using Lean 3. I don't think it should be hard to implement retrieval for Lean 4. I will more than happy if you take this up and finish it. (Can possibly be vibe coded). It will be a great contribution if you can do it @jogobeny