This is a simple modification of the response logic when parse failed occurs.

Lean-gym currently returns a fatal error when parse fails and exits the repl process, which loses all search history. This can occur so easily, that simply inputting an empty line will can cause this issue.

I change the parse_request function that makes it return a fake LeanPEPLRequest containing the parse_failed command and error message. An additional handle_parse_failed function is also added and returns a normal error message without quitting the repl process.

I tested the change in Linux, it works fine.

p.s. great work, looking forward to future updates.

Hi, great work here! But I got some questions when reproducing your paper "Formal Mathematics Statement Curriculum Learning". In this paper, you use the tactic dataset in PACT. However, when I follow the instructions from PACT and create the tactic dataset, most of the tactics and proofs can not reach the "no goals" state when directly applying the tactics in the dataset step by step. Only 30% of them are actually applicable and successfully proven. I wonder if I am doing something wrong here or missing some important steps?

Hi, I wonder how to search a customed theorem with lean-gym? For example, ∀ (a b : ℝ), ∃ x, (a + b) ^ 3 = a ^ 3 + x * a ^ 2 * b + 3 * a * b ^ 2 + b ^ 3. Thanks!

Great job! I want to use lean-gym as an engine to train my AI just like RL gym, but I don't know how to integrate lean-gym with python. Could you please provide an example code? Thanks!

Hi,

Thanks for providing a great tool! I wonder whether it is possible to access the global environment (e.g., existing definitions and theorems either in the same file or imported from other files) using lean-gym. Thanks!

Hi, I have some problems with decreasing performance. Each usage of "run_tac" seems to slow down the usage of further "run_tac"s. At the end is a python file to show the behavior: it repeats (init_search, 2000x run_tac, clear_search) and takes 15s, 17s, 19s, 21s, ... Is there a way around it or should I just reopen lean-gym periodically?

import time
import subprocess
import os
import json

lean_gym_path = os.path.dirname(os.path.realpath(__file__))
lean_gym = subprocess.Popen(['lean', '--run', 'src/repl.lean'],
                            cwd=lean_gym_path,
                            stdin=subprocess.PIPE,
                            stdout=subprocess.PIPE)

def run_lean_cmd(cmd: str):
    lean_gym.stdin.write(cmd.encode('utf-8'))
    lean_gym.stdin.flush()
    return json.loads(lean_gym.stdout.readline().decode('utf-8'))

def init_search(decl: str) -> dict:
    cmd = f'["init_search", ["{decl}", ""]]\n'
    return run_lean_cmd(cmd)

def run_tac(search_id: int, tactic_state_id: int, tactic: str) -> dict:
    cmd = f'["run_tac",["{search_id}","{tactic_state_id}","{tactic}"]]\n'
    return run_lean_cmd(cmd)

def clear_search(search_id: int) -> dict:
    cmd = f'["clear_search",["{search_id}"]]\n'
    return run_lean_cmd(cmd)

t1 = time.time()
for i in range(10000):
    t2 = time.time()
    if i > 1:
        print(t2 - t1)
    t1 = t2

    result = init_search('nat.mul_left_eq_self_iff')
    search_id = int(result['search_id'])
    state_id = int(result['tactic_state_id'])

    result = run_tac(search_id, state_id, 'intros')
    search_id = int(result['search_id'])
    state_id = int(result['tactic_state_id'])

    for state_id in range(1000):
        search_id = int(result['search_id'])
        state_id = int(result['tactic_state_id'])
        result = run_tac(search_id, state_id, 'rw mul_comm')

    clear_search(search_id)

Right now it seems that all proof checks are at the end. This violates the Markovian assumption of Lean gym since a bad tactic upstream can lead to a failure of the final tactic step. Most of the current checks for sorry, undefined, and maybe some of the others are valid checks to do after every proof step. The only one I know for sure won't work is the metavariable check. That isn't supposed to hold until a proof is complete.