~

index.html

@@ -358,6 +358,7 @@ <h2 class="title is-3"><span class="dvima">Benchmarks</span></h2>
             <div class="rows is-centered ">
                 <div class="row is-full-width">
                     <h2 class="title is-3"><span class="dvima">Interacting with Lean</span></h2>
+                    <img src="images/interaction.jpg" class="interpolation-image" alt="" style="display: block; margin-left: auto; margin-right: auto"/>
                     <p style="font-size: 125%">LeanDojo turns Lean into a <a target="_blank" href="https://github.com/openai/gym">gym-like</a> 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.</p>
                 </div>
             </div>