openai/lean-gym

This is stars and forks stats for /openai/lean-gym repository. As of 08 May, 2024 this repository has 120 stars and 31 forks.

lean-gym This repository lets you interact with Lean through a REPL. See Formal Mathematics Statement Curriculum Learning for a presentation of lean-gym. Setup # Download pre-built binaries and build the project (targeting mathlib). bash ./scripts/setup.sh Usage lean --run src/repl.lean Starts a fresh REPL. Once started, the REPL accepts the following commands: init_search: takes a declaration name as well as a list of open namespaces to initialize a search at the given declaration opening the provided...