From 958b29f6fe7b6666962bd5998da6c3ba197c2f5d Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@cs.princeton.edu>
Date: Mon, 26 Jun 2023 12:50:30 -0500
Subject: [PATCH] ~

---
 index.html | 1 +
 1 file changed, 1 insertion(+)

diff --git a/index.html b/index.html
index 72e9aec..a4a53a5 100644
--- a/index.html
+++ b/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>