Lean REPL

Stream: lean-gptf

[Stanislas Polu]

Stanislas Polu said:

We've just open-sourced our new REPL (based on Jesse Michael Han's lean-gptf) for Lean 3 loosely following Mario Carneiro's proposed interface. It exposes a JSON interface easy to integrate from your language of choice:

$ lean --run src/repl.lean

["init_search", ["int.prime.dvd_mul", ""]]
{"error":null,"search_id":"0","tactic_state":"⊢ ∀ {m n : ℤ} {p : ℕ}, nat.prime p → ↑p ∣ m * n → p ∣ m.nat_abs ∨ p ∣ n.nat_abs","tactic_state_id":"0"}

["run_tac",["0","0","intros"]]
{"error":null,"search_id":"0","tactic_state":"m n : ℤ,\tp : ℕ,\thp : nat.prime p,\th : ↑p ∣ m * n\t⊢ p ∣ m.nat_abs ∨ p ∣ n.nat_abs","tactic_state_id":"1"}

["run_tac",["0","1","apply (nat.prime.dvd_mul hp).mp"]]
{"error":null,"search_id":"0","tactic_state":"m n : ℤ,\tp : ℕ,\thp : nat.prime p,\th : ↑p ∣ m * n\t⊢ p ∣ m.nat_abs * n.nat_abs","tactic_state_id":"2"}

["run_tac",["0","2","rw ← int.nat_abs_mul"]]
{"error":null,"search_id":"0","tactic_state":"m n : ℤ,\tp : ℕ,\thp : nat.prime p,\th : ↑p ∣ m * n\t⊢ p ∣ (m * n).nat_abs","tactic_state_id":"3"}

["run_tac",["0","3","simp"]]
{"error":"run_tac_failed: pos=(some ⟨1, 2⟩) msg=simplify tactic failed to simplify","search_id":null,"tactic_state":null,"tactic_state_id":null}

["run_tac",["0","3","exact int.coe_nat_dvd_left.mp h"]]
{"error":null,"search_id":"0","tactic_state":"no goals","tactic_state_id":"4"}

It smoothly handles and return tactic application errors and allows multiplexing of proof searches on a single REPL (interleaving of run_tac and init_search commands). It is still subject to a few crashes, but empirically they happen less than 0.01% of the time, which is within bound for a production use at scale. We've successfully run pools of 128+ REPLs each multiplexing 64+ searches in parallel.

Hopefully, this will help make Lean 3 (and surely 4 very soon) a prime choice for machine learning research.

The project is hosted here: https://github.com/openai/lean-gym -- Contributions and feedback welcome!