diff --git a/index.html b/index.html index 72e9aec..a4a53a5 100644 --- a/index.html +++ b/index.html @@ -358,6 +358,7 @@

Benchmarks

Interacting with Lean

+

LeanDojo turns Lean into a gym-like environment, in which the prover can observe the proof state, run tactics to change the state, and receive feedback on errors or on proof completion. This environment is indispensable for evaluating/deploying the prover or training it through RL.