partI_nextstep/notebooks/I_nextstep_lean__part3_proofsearch.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Neural next-step prediction | part 3: proof search\n",
    "Tutorial on neural theorem proving\\\n",
    "Author: Sean Welleck\n",
    "\n",
    "----------------\n",
    "\n",
    "#### High-level goal\n",
    "\n",
    "Our next goal is to prove theorems with our neural next-step predictor, and check whether the theorems are correct.\n",
    "\n",
    "Proving and checking a theorem involves generating a next-step candidate with our model, giving it to Lean, and receiving a next state from Lean (or an error message). \\\n",
    "To do so, we will need two components:\n",
    "\n",
    "1. **Interacting** with Lean:  an automated way to give a next-step to Lean and receive a next state (or an error).\n",
    "<!--  -->\n",
    "2. A **search strategy** that uses the next-step model and Lean to find a proof (e.g. generate one next-step, get the next state, repeat).\n",
    "<!-- For example, a naive algorithm alternates between generating a single step, giving it to Lean, and continuing until a proof is complete or an error message is reached. One can imagine many other strategies, e.g. generating *multiple* next steps and choosing the 'best' one according to some criterion, backtracking upon receiving an error message, etc. -->\n",
    "\n",
    "Below, we'll walk through a simple example of each. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "-------------------\n",
    "\n",
    "### 1. Interaction\n",
    "\n",
    "To start, we'll walk through proving this theorem:"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "```lean4\n",
    "import Mathlib.Data.Nat.Prime\n",
    "\n",
    "example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by\n",
    "  apply le_trans h₀\n",
    "  apply h₁\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Interaction with `Lean REPL`\n",
    "\n",
    "The [`Lean REPL`](https://github.com/zhangir-azerbayev/repl/tree/master) gives us a programmatic interface to communicate with Lean.\n",
    "\n",
    "We make a lightweight Python wrapper (based on code from the [pylean](https://github.com/zhangir-azerbayev/repl/tree/master) repo).\n",
    "\n",
    "\n",
    "Set `PATH_TO_REPL` to the `ntp-interact/repl` directory (contained in this repository):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "PATH_TO_REPL = '/Users/wellecks/projects/ntptutorial/partI_nextstep/ntp-interact/repl'"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "import pexpect\n",
    "import json\n",
    "\n",
    "import os\n",
    "\n",
    "class LeanServer:\n",
    "    # Based on code from the [pylean](https://github.com/zhangir-azerbayev/repl/tree/master) repo\n",
    "    def __init__(self, path_to_repl):\n",
    "        self.proc = pexpect.spawn(\n",
    "            \"lake env lean --run REPL/Main.lean\", cwd=path_to_repl, encoding=\"utf-8\")\n",
    "\n",
    "    def run_code(self, code, env=None, verbose=False):\n",
    "        if env:\n",
    "            command = (\n",
    "                json.dumps(dict(cmd=code, env=env))\n",
    "            )  \n",
    "        else:\n",
    "            command = (\n",
    "                '{ \"cmd\" : \"' + repr(code)[1:-1] + '\" }'\n",
    "            )  \n",
    "\n",
    "        if verbose:\n",
    "            print(command)\n",
    "        self.proc.sendline(command)\n",
    "        self.proc.expect_exact(command + \"\\r\\n\")\n",
    "        self.proc.sendline()\n",
    "        self.proc.expect_exact(\"\\r\\n\")\n",
    "        try:\n",
    "            index = self.proc.expect('env\": \\d+\\}', timeout=20)\n",
    "            output = self.proc.before + self.proc.match.group()\n",
    "            if verbose: \n",
    "                print(output)\n",
    "            return json.loads(output)\n",
    "        except pexpect.exceptions.TIMEOUT:\n",
    "            raise pexpect.exceptions.TIMEOUT"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now we can submit Lean code (e.g., imports, theorem declarations) and receive messages from Lean:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{'env': 0,\n",
      " 'messages': [{'data': 'unsolved goals\\n'\n",
      "                       'x y z : ℝ\\n'\n",
      "                       'h₀ : x ≤ y\\n'\n",
      "                       'h₁ : y ≤ z\\n'\n",
      "                       '⊢ x ≤ z',\n",
      "               'endPos': {'column': 62, 'line': 6},\n",
      "               'pos': {'column': 61, 'line': 6},\n",
      "               'severity': 'error'}]}\n"
     ]
    }
   ],
   "source": [
    "from pprint import pprint\n",
    "\n",
    "code = \"\"\"\n",
    "import Mathlib\n",
    "\n",
    "open Real\n",
    "\n",
    "example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by {}\n",
    "\"\"\"\n",
    "\n",
    "\n",
    "lean = LeanServer(PATH_TO_REPL)\n",
    "msg = lean.run_code(code)\n",
    "lean.proc.close()\n",
    "pprint(msg)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We see that inside of `'data'`, the Lean REPL gives us the current proof state $x_t$; here's basic parsing code:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x y z : ℝ\n",
      "h₀ : x ≤ y\n",
      "h₁ : y ≤ z\n",
      "⊢ x ≤ z\n"
     ]
    }
   ],
   "source": [
    "def get_goal(msg):\n",
    "    goal = None\n",
    "    for msg_ in msg['messages']:\n",
    "        if msg_['data'].startswith('unsolved goals\\n'):\n",
    "            goal = '\\n'.join(msg_['data'].split('\\n')[1:])\n",
    "        elif msg_['severity'] == 'error':\n",
    "            return None\n",
    "    return goal\n",
    "\n",
    "print(get_goal(msg))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can use $x_t$ as input to our model $p_\\theta(y_t|x_t)$.\\\n",
    "Next, we load the trained model and generate a next step, $\\hat y_t\\sim q(p_\\theta(y_t|x_t))$.\n",
    "\n",
    "(Here $q(\\cdot)$ is a decoding algorithm such as greedy decoding or temperature sampling.)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "Special tokens have been added in the vocabulary, make sure the associated word embeddings are fine-tuned or trained.\n"
     ]
    }
   ],
   "source": [
    "# Load model and tokenizer\n",
    "import os\n",
    "import transformers\n",
    "os.environ['TOKENIZERS_PARALLELISM'] = 'false'  # prevents an annoying warning\n",
    "\n",
    "MODEL = 'l3lab/ntp-mathlib-st-deepseek-coder-1.3b'\n",
    "model = transformers.AutoModelForCausalLM.from_pretrained(MODEL)\n",
    "tokenizer = transformers.AutoTokenizer.from_pretrained(MODEL)\n",
    "\n",
    "def generate(prompt):\n",
    "    input_ids = tokenizer.encode(prompt, return_tensors='pt')\n",
    "    out = model.generate(\n",
    "        input_ids,\n",
    "        max_new_tokens=256,\n",
    "        pad_token_id=tokenizer.eos_token_id,\n",
    "    )\n",
    "    text = tokenizer.decode(out[0][input_ids.shape[1]:], skip_special_tokens=True).split('[/TAC')[0].strip()\n",
    "    return text"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      " linarith\n"
     ]
    }
   ],
   "source": [
    "# Generate a next step\n",
    "prompt = \"\"\"/- You are proving a theorem in Lean 4.\n",
    "You are given the following information:\n",
    "- The current proof state, inside [STATE]...[/STATE]\n",
    "\n",
    "Your task is to generate the next tactic in the proof.\n",
    "Put the next tactic inside [TAC]...[/TAC]\n",
    "-/\n",
    "[STATE]\n",
    "%s\n",
    "[/STATE]\n",
    "[TAC]\n",
    "\"\"\" % get_goal(msg)\n",
    "\n",
    "prefix = ''\n",
    "next_step = prefix + ' ' + generate(prompt + prefix)\n",
    "print(next_step)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Finally, we can give the generated next step to Lean and receive the next state."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{'env': 0}\n"
     ]
    }
   ],
   "source": [
    "code = \"\"\"\n",
    "import Mathlib\n",
    "\n",
    "open Real\n",
    "\n",
    "example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by\n",
    "\"\"\" + next_step\n",
    "\n",
    "lean = LeanServer(PATH_TO_REPL)\n",
    "state = lean.run_code(code)\n",
    "lean.proc.close()\n",
    "\n",
    "pprint(state)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "There are no error messages, and no remaining goals - the proof is complete! If you want, paste this into VS Code to convince yourself that it's complete:\n",
    "\n",
    "```lean4\n",
    "import Mathlib.Data.Nat.Prime\n",
    "\n",
    "example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by\n",
    "  linarith\n",
    "```\n",
    "\n",
    "Also, notice that the machine-generated proof is different from the human written one shown at the starting of this section.\n",
    "\n",
    "\n",
    "**Exercise I:** modify the `prefix` variable above to obtain an invalid proof.\n",
    "\n",
    "**Exercise II:** modify the `prefix` variable above to obtain an alternative, valid one-step proof."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "-----------------\n",
    "\n",
    "### 2. Search strategy\n",
    "\n",
    "In the proof above, we simply generated one next step and the proof was complete.\n",
    "\n",
    "In general, proofs are multiple steps. Therefore we need an algorithm for generating a multiple step proof, which we refer to as a *search algorithm*.\n",
    "\n",
    "\n",
    "First, let's consider a naive algorithm that generates a next step, then continues to the next state. Upon receiving an error message\n",
    "the algorithm generates another next step."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [],
   "source": [
    "import sys\n",
    "sys.path.append('../ntp-interact/')\n",
    "\n",
    "import proofsearch # some utilities for running code (as we did above) and parsing states/model outputs"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "== Current (0): \n",
      "theorem thm1 (a b c : Nat) : a + b = c → a ≤ c := by\n",
      "\n",
      "-- Goal: \n",
      "a b c : ℕ\n",
      "⊢ a + b = c → a ≤ c\n",
      "\n",
      "== Current (1): \n",
      "theorem thm1 (a b c : Nat) : a + b = c → a ≤ c := by\n",
      "rintro rfl\n",
      "-- Goal: \n",
      "a b : ℕ\n",
      "⊢ a ≤ a + b\n",
      "\n",
      "== Current (2): \n",
      "theorem thm1 (a b c : Nat) : a + b = c → a ≤ c := by\n",
      "rintro rfl\n",
      "simp\n",
      "\n",
      "SUCCESS!\n",
      "theorem thm1 (a b c : Nat) : a + b = c → a ≤ c := by\n",
      "  rintro rfl\n",
      "  simp\n"
     ]
    }
   ],
   "source": [
    "transformers.set_seed(42)\n",
    "\n",
    "def _prompt_fn(goal):\n",
    "    return \"\"\"/- You are proving a theorem in Lean 4.\n",
    "You are given the following information:\n",
    "- The current proof state, inside [STATE]...[/STATE]\n",
    "\n",
    "Your task is to generate the next tactic in the proof.\n",
    "Put the next tactic inside [TAC]...[/TAC]\n",
    "-/\n",
    "[STATE]\n",
    "%s\n",
    "[/STATE]\n",
    "[TAC]\n",
    "\"\"\" % goal\n",
    "\n",
    "def prove_simple(model, tokenizer, header, theorem_statement, search_budget):\n",
    "    success = False\n",
    "\n",
    "    code = header + theorem_statement\n",
    "    steps = []\n",
    "    proof = ''\n",
    "\n",
    "    for i in range(search_budget):\n",
    "        print(\"== Current (%d): \" % i, theorem_statement[:-3] + '\\n' + proof, sep='\\n')\n",
    "\n",
    "        # Run the code (header + proof-so-far)\n",
    "        state = proofsearch.run_code(code, path_to_repl=PATH_TO_REPL)\n",
    "        \n",
    "        # Stop if the proof is complete.\n",
    "        if proofsearch.is_done(state):\n",
    "            success = True\n",
    "            break\n",
    "\n",
    "        # Get the new state.\n",
    "        goal_candidate = proofsearch.get_goal(state)\n",
    "        if goal_candidate is None:\n",
    "            print(\"-- Error: backtracking\")\n",
    "            steps = steps[:-1]\n",
    "        else:\n",
    "            goal = goal_candidate\n",
    "\n",
    "        print(\"-- Goal: \", goal, sep='\\n')\n",
    "\n",
    "        # Generate a next-step\n",
    "        prompt = _prompt_fn(goal)\n",
    "        texts, _= proofsearch.generate(\n",
    "            prompt, model, tokenizer, temperatures=[0.5], num_samples=1,\n",
    "            stop=['[/TAC]']\n",
    "            )\n",
    "        step = proofsearch.parse_step(texts[0])\n",
    "\n",
    "        # Add the next-step to the proof-so-far\n",
    "        steps.append(step)\n",
    "        proof = '\\n'.join(steps)\n",
    "        code = header + theorem_statement.replace(\" {}\", \"\") + '\\n' + proof\n",
    "        print()\n",
    "\n",
    "    if success:\n",
    "        print(\"\\nSUCCESS!\")\n",
    "    else:\n",
    "        print(\"\\nFAILED\")\n",
    "    \n",
    "    print(theorem_statement.replace(\" {}\", \"\"))\n",
    "    print ('  ' + proof.replace('\\n', '\\n  '))\n",
    "    \n",
    "    return {'theorem_statement': theorem_statement, 'proof': proof, 'success': success}\n",
    "\n",
    "\n",
    "header = \"\"\"\n",
    "import Mathlib.Data.Nat.Prime\n",
    "\n",
    "\"\"\"\n",
    "theorem_statement = \"\"\"theorem thm1 (a b c : Nat) : a + b = c → a ≤ c := by {}\"\"\"\n",
    "\n",
    "\n",
    "out = prove_simple(\n",
    "    model, \n",
    "    tokenizer,\n",
    "    header, \n",
    "    theorem_statement, \n",
    "    search_budget=100\n",
    ")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Above the model first generates `rintro rfl`, and receives a new proof state.\\\n",
    "Then it generates `simp` and the proof is complete."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Best-first search\n",
    "\n",
    "Typically a less naive search procedure is used. These searches are usually variants of a tree search, in which nodes are states and edges are next-steps. \n",
    "\n",
    "The most common search in neural theorem proving is *best-first search*. This search:\n",
    "\n",
    "- generates multiple next-step suggestions to form (proof-so-far + next-step) *candidates*\n",
    "- scores all candidates so far\n",
    "- selects the highest scoring candidate\n",
    "\n",
    "A typical scoring function is the model's log probability, $\\log p_\\theta(y_t|x_t)$, summed across steps. Next-steps that lead to an error receive a score of $-\\infty$ (in practice, we discard these steps). In the literature, the scoring function is called a *value function* $v(y_{\\leq t}, x_t)$.\n",
    "\n",
    "#### Intuition\n",
    "\n",
    "A key idea is generating multiple suggestions at each step, ${y_t^{(1)},\\ldots,y_t^{(k)}}\\sim p_\\theta(\\cdot|x_t)$. Intuitively, the goal is to select a next-step that will lead to a correct proof. In general, we do not know whether a next-step will lead to a correct proof, so we use a heuristic value function for selecting a next-step.\n",
    "\n",
    "Here's what multiple suggestions and their (normalized) log-probabilities look like in our example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "-0.131\trintro rfl\n",
      "[/TAC]\n",
      "-0.346\tintro h\n",
      "[/TAC]\n",
      "-0.372\trintro ⟨⟩\n",
      "[/TAC]\n",
      "-0.580\tsimpa only [Nat.zero_add] using le_of_add_le_add_left\n",
      "[/TAC]\n",
      "-0.604\trw [add_comm, add_le_add_iff_right]\n",
      "[/TAC]\n",
      "-0.686\tlet g : ℕ → ℕ → Prop := fun a b ↦ (a + b = c)\n",
      "[/TAC]\n"
     ]
    }
   ],
   "source": [
    "transformers.set_seed(40)\n",
    "\n",
    "prompt = _prompt_fn(goal=\"\"\"a b c : ℕ\\n⊢ a + b = c → a ≤ c\"\"\")\n",
    "texts, scores = proofsearch.generate(prompt, model, tokenizer, temperatures=[1.0], num_samples=10, stop=['[/TAC]'])\n",
    "for text, score in zip(texts, scores):\n",
    "    text = text.strip()\n",
    "    print('%.3f' % score, text, sep='\\t')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Implementation\n",
    "\n",
    "A minimal implementation of best first search is available in `proofsearch.py`.\n",
    "\n",
    "We will use this in the next notebook to evaluate our model on a set of evaluation theorems.\\\n",
    "Below, we run best first search and print out the search trajectory:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- current:\n",
      "\ttheorem thm1 (a b c : Nat) : a + b = c → a ≤ c := by \n",
      "\t\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|███████████████████████████████████████████████████████████████████████████████████████████| 4/4 [00:01<00:00,  2.08it/s]\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- type-checked candidates:\n",
      "\t(-0.131) rintro rfl\n",
      "\t(-0.131) rintro rfl\n",
      "\t(-0.346) intro h\n",
      "\t(-0.372) rintro ⟨⟩\n",
      "--- current:\n",
      "\ttheorem thm1 (a b c : Nat) : a + b = c → a ≤ c := by \n",
      "\trintro rfl\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|███████████████████████████████████████████████████████████████████████████████████████████| 4/4 [00:01<00:00,  2.07it/s]"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- type-checked candidates:\n",
      "\t(-0.325) simp\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "{'theorem_statement': 'theorem thm1 (a b c : Nat) : a + b = c → a ≤ c := by {}',\n",
       " 'proof': ['rintro rfl', 'simp'],\n",
       " 'state': {'env': 0},\n",
       " 'score': 0.4551752954721451,\n",
       " 'success': True}"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "proofsearch.best_first_search(\n",
    "    model, tokenizer, header, theorem_statement, \n",
    "    max_iters=32,\n",
    "    num_samples=4,\n",
    "    temperatures=[0.0],\n",
    "    verbose=True,\n",
    "    path_to_repl=PATH_TO_REPL\n",
    ")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The search selects a candidate trajectory, and generates 4 next-step suggestions.\\\n",
    "`rintro rfl` is selected at the first step because it has the best score. \\\n",
    "The best expansion of `rintro rfl` is `simp`. `simp` completes the proof, so the proof terminates.\n",
    "\n",
    "\n",
    "**Exercise:** suppose that `simp` did not complete the proof. Which tactic would be expanded next?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "--------------------\n",
    "\n",
    "\n",
    "## Extensions\n",
    "\n",
    "Several works have proposed to improve the search strategy, either with a learned value function or a sophisticated search:\n",
    "\n",
    "- [Polu & Sutskever 2020](https://arxiv.org/pdf/2009.03393.pdf) propose to learn a value function $v(y_{\\leq t}, x_t)$ that estimates the probability of successfully proving the theorem with the model $p_\\theta$ starting at state $x_t$. To do so, they use proof search trajectories obtained by doing proof search with the model.\n",
    "\n",
    "- [Polu et al ICLR 2023](https://openreview.net/pdf?id=-P7G-8dmSh4) train the value function to predict the eventual length of the proof (or 0 if it is predicted to fail). The learned value function improves pass rate by ~10\\% on mathlib theorems compared to log-probability, with a ~1\\% improvement over the learned value function from [Polu & Sutskever 2020].\n",
    "\n",
    "- [Lample et al NeurIPS 2022](https://openreview.net/pdf?id=J4pX8Q8cxHH) propose a sophisticated MCTS-like search that explores multiple trajectories in parallel, collecting statistics on visited states in order to prioritize search trajectories.\n",
    "\n",
    "Reproducing, analyzing, and improving the search algorithm remains an open area for future work in neural theorem proving (for instance, these works were not open-sourced).\n",
    "\n",
    "Search algorithms are also an active area of research in LLMs, including methods like [tree-of-thought](https://arxiv.org/abs/2305.10601), [stepwise beam search](https://arxiv.org/pdf/2205.12910.pdf), [self-consistency](https://arxiv.org/pdf/2203.11171.pdf), and search with [learned stepwise verifiers](https://arxiv.org/pdf/2305.20050.pdf). In theorem proving, the final output is verifiable, but the quality of intermediate steps is difficult to evaluate."
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.13"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}