partI_nextstep/notebooks/I_nextstep_lean__part5_context.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Neural next-step prediction | part 5: theorem proving with context\n",
    "Tutorial on neural theorem proving\\\n",
    "Author: Sean Welleck\n",
    "\n",
    "----------------\n",
    "\n",
    "#### High-level goal\n",
    "\n",
    "In this notebook we will train and evaluate theorem provers that use additional context, $p_\\theta(y_t|x_t,c)$, such as the preceding file contents. \\\n",
    "This will enable support for several real-world scenarios that we discuss next.\n",
    "\n",
    "*Historical note*: the setting described here was first investigated in [LLMstep: proofstep suggestions in Lean](https://mathai2023.github.io/papers/40.pdf).\n",
    "\n",
    "### Motivation\n",
    "\n",
    "Real-world proofs often use theorems and definitions that are unique to the proof development. A key\n",
    "limitation of the models that we have considered  is that they lack context beyond the current proof state. That\n",
    "is, the model $p_\\theta(y_t|x_t)$ only receives the current proof state $x_t$ (transformed into a prompt) as input. \n",
    "\n",
    "As a result, the model cannot use newly defined theorems, definitions, and other information from the current proof development,\n",
    "unless the proof development was seen during training. To see this, we will look at a toy example, followed by a real-world example.\n",
    "\n",
    "#### Toy Example \n",
    "\n",
    "The situation below shows the need for incorporating additional context $c$ beyond the proof state.\n",
    "\n",
    "Namely, proving the `my_object_sum_nonneg` theorem requires using properties (in pink) of the newly defined `my_object` (in green):\n",
    "\n",
    "<img src=\"images/context_1.png\" width=500px>\n",
    "\n",
    "\n",
    "The next-step predictors we have trained will almost certainly fail unless they have seen `my_object_sum_nonneg` in their training set. Not surprisingly, our existing model does not successfully prove this theorem:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "PATH_TO_REPL = '/Users/wellecks/projects/ntptutorial/partI_nextstep/ntp-interact/repl'\n",
    "\n",
    "import sys\n",
    "sys.path.append('../ntp-interact/')\n",
    "\n",
    "import proofsearch\n",
    "import os\n",
    "import transformers\n",
    "os.environ['TOKENIZERS_PARALLELISM'] = 'false'  # prevents an annoying warning"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "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"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- current:\n",
      "\ttheorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by \n",
      "\t\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|██████████| 8/8 [00:14<00:00,  1.87s/it]\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- type-checked candidates:\n",
      "\t(-0.384) rw [add_comm]\n",
      "\t(-0.473) simp\n",
      "--- current:\n",
      "\ttheorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by \n",
      "\trw [add_comm]\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|██████████| 8/8 [00:08<00:00,  1.00s/it]\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- type-checked candidates:\n",
      "\t(-0.489) simp\n",
      "--- current:\n",
      "\ttheorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by \n",
      "\tsimp\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|██████████| 5/5 [00:03<00:00,  1.39it/s]\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- type-checked candidates:\n",
      "\t(-0.373) apply add_nonneg\n",
      "--- current:\n",
      "\ttheorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by \n",
      "\tsimp\n",
      "\tapply add_nonneg\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|██████████| 6/6 [00:03<00:00,  1.55it/s]\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- type-checked candidates:\n",
      "\t\n",
      "--- current:\n",
      "\ttheorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by \n",
      "\trw [add_comm]\n",
      "\tsimp\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|██████████| 8/8 [00:07<00:00,  1.08it/s]\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- type-checked candidates:\n",
      "\t(-0.356) rw [add_comm]\n",
      "\t(-0.363) apply add_nonneg\n",
      "--- current:\n",
      "\ttheorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by \n",
      "\trw [add_comm]\n",
      "\tsimp\n",
      "\tapply add_nonneg\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|██████████| 8/8 [00:14<00:00,  1.75s/it]"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- type-checked candidates:\n",
      "\t\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "{'theorem_statement': 'theorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by {}',\n",
       " 'success': False}"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "\n",
    "MODEL = 'l3lab/ntp-mathlib-st-deepseek-coder-1.3b'\n",
    "model, tokenizer = proofsearch.load_model(MODEL)\n",
    "\n",
    "\n",
    "header = \"\"\"import Mathlib\n",
    "\n",
    "open BigOperators\n",
    "\n",
    "variable {Ω : Type*}[Fintype Ω]\n",
    "\n",
    "structure my_object (Ω : Type*)[Fintype Ω] :=\n",
    "  (f : Ω → ℝ)\n",
    "  (cool_property : ∀ x : Ω, 0 ≤ f x)\n",
    "\n",
    "\"\"\"\n",
    "transformers.set_seed(40)\n",
    "\n",
    "theorem_statement = \"\"\"theorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by {}\"\"\"\n",
    "proofsearch.best_first_search(\n",
    "    model, tokenizer, header, theorem_statement, \n",
    "    max_iters=16,\n",
    "    num_samples=8,\n",
    "    temperatures=[0.5],\n",
    "    verbose=True,\n",
    "    path_to_repl=PATH_TO_REPL\n",
    ")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Example from [Terence Tao's PFR project]( ) \n",
    "\n",
    "Analogous situations occur in almost every real-world theorem proving scenario.\n",
    "\n",
    "For instance, consider the beginning of this file from Terence Tao's formalization of the [Polynomial Freiman-Ruzsa Conjecture](https://github.com/teorth/pfr/blob/master/PFR) (PFR):\n",
    "- [Entropy/Basic.lean](https://github.com/teorth/pfr/blob/master/PFR/ForMathlib/Entropy/Basic.lean)\n",
    "\n",
    "It has a new definition (green), new notation (orange), and new theorems/lemmas (pink) that are used frequently:\n",
    "\n",
    "<img src=\"images/context_2.png\" width=\"650px\">\n",
    "\n",
    "*Exercise*: look through other files in [PFR](https://github.com/teorth/pfr/blob/master/PFR), and consider the following questions:\n",
    "1. How often do theorems use definitions that are newly defined in PFR (e.g., in the current file or other files)?\n",
    "\n",
    "2. How often do proofs use new definitions, lemmas, or theorems that are defined in PFR?\n",
    "\n",
    "3. Suppose that PFR is not in the language model's training or fine-tuning set. \\\n",
    "What are the implications of (1), and (2) for using the language model to suggest proofs in PFR?\n",
    "\n",
    "4. Navigate to the bottom of some files. \\\n",
    "Can you find a theorem or proof that depends on multiple pieces of context? \\\n",
    "Can you find a theorem or proof that depends on context that is \"far away\" from the theorem declaration?\n",
    "\n",
    "5. Suppose that the language model was finetuned with a context length of around 4000 tokens. \\\n",
    "What are the implications of (4) for using the language model to suggest proofs in PFR?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Theorem prover with context"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To this end, we will train a model of the form:\n",
    "\n",
    "\\begin{align}\n",
    "p_\\theta(y_t|x_t,c_t),\n",
    "\\end{align}\n",
    "\n",
    "where $x_t$ is the proof state, $c_t$ is the preceding file contents up to the current tactic, and $y_t$ is a next tactic.\n",
    "\n",
    "Doing so amounts to generating new instruction tuning data that includes new prompts:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "/- You are proving a theorem in Lean 4.\n",
      "You are given the following information:\n",
      "- The file contents up to the current tactic, inside [CTX]...[/CTX]\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",
      "[CTX]\n",
      "import Mathlib.Data.Nat.Prime\n",
      "\n",
      "theorem test_thm (m n : Nat) (h : m.Coprime n) : m.gcd n = 1 := by\n",
      "  \n",
      "[/CTX]\n",
      "[STATE]\n",
      "m n : ℕ\n",
      "h : Nat.Coprime m n\n",
      "⊢ Nat.gcd m n = 1\n",
      "[/STATE]\n",
      "[TAC]\n",
      "\n",
      "rw [Nat.Coprime] at h\n",
      "[/TAC]\n"
     ]
    }
   ],
   "source": [
    "import sys\n",
    "import jsonlines\n",
    "sys.path.append('../ntp-training-data/scripts')\n",
    "\n",
    "from instruction_tuning import prompt_context_state_tactic\n",
    "\n",
    "example = next(jsonlines.Reader(open('../ntp-training-data/example0.jsonl')).iter())\n",
    "prompt, completion = prompt_context_state_tactic(example, truncation=1024)\n",
    "\n",
    "print(prompt)\n",
    "print(completion)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here is the command for running the script on the extracted data from Mathlib:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "# !cd ../ntp-training-data && python scripts/instruction_tuning.py --context-truncation 1024 --name with_context --output-base-dir instructions/with_context --prompt context_state_tactic state_tactic --mathlib-only"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If you would like to finetune your own model, you can follow the same procedure as in part 2, which would use code in the [ntp-tune](../ntp-tune/) directory. Finetuning would require changing the `TRAIN_FILE` and `VALID_FILE` filepaths in the [finetune.sh](../ntp-tune/finetune.sh) script to point to the new instruction tuning data. \n",
    "\n",
    "\n",
    "We provide the instruction tuning data and a fine-tuned model on HuggingFace:\n",
    "\n",
    "- [`l3lab/ntp-mathlib-instruct-context`](https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-context) (Data)\n",
    "- [`l3lab/ntp-mathlib-context-deepseek-coder-1.3b`](https://huggingface.co/l3lab/ntp-mathlib-context-deepseek-coder-1.3b) (Model)\n",
    "\n",
    "We evaluated this model on miniF2F and it closed 29.5% (72/244) of proofs."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Theorem proving with context\n",
    "\n",
    "Now let's use the model to prove the theorem in the toy example from above:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "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"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- current:\n",
      "\ttheorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by \n",
      "\t\n",
      "/- You are proving a theorem in Lean 4.\n",
      "You are given the following information:\n",
      "- The file contents up to the current tactic, inside [CTX]...[/CTX]\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",
      "[CTX]\n",
      "import Mathlib\n",
      "\n",
      "open BigOperators\n",
      "\n",
      "variable {Ω : Type*}[Fintype Ω]\n",
      "\n",
      "structure my_object (Ω : Type*)[Fintype Ω] :=\n",
      "  (f : Ω → ℝ)\n",
      "  (cool_property : ∀ x : Ω, 0 ≤ f x)\n",
      "\n",
      "theorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by \n",
      "[/CTX]\n",
      "[STATE]\n",
      "Ω : Type u_1\n",
      "inst✝ : Fintype Ω\n",
      "o1 o2 : my_object Ω\n",
      "⊢ o1.f + o2.f ≥ 0\n",
      "[/STATE]\n",
      "[TAC]\n",
      "\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|██████████| 8/8 [00:14<00:00,  1.85s/it]\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- type-checked candidates:\n",
      "\t(-0.216) apply add_nonneg\n",
      "\t(-0.206) simp [o1.cool_property, o2.cool_property]\n",
      "--- current:\n",
      "\ttheorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by \n",
      "\tsimp [o1.cool_property, o2.cool_property]\n",
      "/- You are proving a theorem in Lean 4.\n",
      "You are given the following information:\n",
      "- The file contents up to the current tactic, inside [CTX]...[/CTX]\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",
      "[CTX]\n",
      "import Mathlib\n",
      "\n",
      "open BigOperators\n",
      "\n",
      "variable {Ω : Type*}[Fintype Ω]\n",
      "\n",
      "structure my_object (Ω : Type*)[Fintype Ω] :=\n",
      "  (f : Ω → ℝ)\n",
      "  (cool_property : ∀ x : Ω, 0 ≤ f x)\n",
      "\n",
      "theorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by simp [o1.cool_property, o2.cool_property]\n",
      "[/CTX]\n",
      "[STATE]\n",
      "Ω : Type u_1\n",
      "inst✝ : Fintype Ω\n",
      "o1 o2 : my_object Ω\n",
      "⊢ 0 ≤ o1.f + o2.f\n",
      "[/STATE]\n",
      "[TAC]\n",
      "\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "100%|██████████| 7/7 [00:14<00:00,  2.10s/it]"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- type-checked candidates:\n",
      "\t(-0.136) exact add_nonneg o1.cool_property o2.cool_property\n"
     ]
    },
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "{'theorem_statement': 'theorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by {}',\n",
       " 'proof': ['simp [o1.cool_property, o2.cool_property]',\n",
       "  'exact add_nonneg o1.cool_property o2.cool_property'],\n",
       " 'state': {'env': 0},\n",
       " 'score': 0.3417195677757263,\n",
       " 'success': True}"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "MODEL = 'l3lab/ntp-mathlib-context-deepseek-coder-1.3b'\n",
    "\n",
    "model, tokenizer = proofsearch.load_model(MODEL)\n",
    "\n",
    "header = \"\"\"import Mathlib\n",
    "\n",
    "open BigOperators\n",
    "\n",
    "variable {Ω : Type*}[Fintype Ω]\n",
    "\n",
    "structure my_object (Ω : Type*)[Fintype Ω] :=\n",
    "  (f : Ω → ℝ)\n",
    "  (cool_property : ∀ x : Ω, 0 ≤ f x)\n",
    "\n",
    "\"\"\"\n",
    "\n",
    "theorem_statement = \"\"\"theorem my_object_sum_nonneg (o1 o2: my_object Ω) : o1.f + o2.f ≥ 0 := by {}\"\"\"\n",
    "\n",
    "transformers.set_seed(42)\n",
    "proofsearch.best_first_search(\n",
    "    model, tokenizer, header, theorem_statement, \n",
    "    max_iters=16,\n",
    "    num_samples=8,\n",
    "    temperatures=[0.5],\n",
    "    verbose=True,\n",
    "    # -- KEY DIFFERENCE: now we add the header + statement to the prompt\n",
    "    prompt_fn=proofsearch.prompt_with_context,\n",
    "    context=header + theorem_statement.replace(\"{}\", \"\"),\n",
    "    # -----\n",
    "    path_to_repl=PATH_TO_REPL\n",
    ")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Evaluating on real examples\n",
    "\n",
    "Finally, let's attempt to prove a few real (context, theorem) examples from [Math2001](https://github.com/teorth/pfr).\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "evaluation_theorems = [\n",
    "    (\"\"\"/- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/\n",
    "import Mathlib.Data.Real.Basic\n",
    "import Mathlib\n",
    "     \n",
    "open BigOperators\n",
    "\n",
    "def Superpowered (k : ℕ) : Prop := ∀ n : ℕ, Prime (k ^ k ^ n + 1)\n",
    "\n",
    "\"\"\", \n",
    "\"\"\"theorem not_superpowered_zero : ¬ Superpowered 0 := by {}\"\"\"),\n",
    "\n",
    "(\"\"\"import Mathlib.Data.Real.Basic\n",
    "import Mathlib\n",
    "\n",
    "open Function\n",
    "namespace Int\n",
    "\n",
    "\n",
    "def F : ℕ → ℤ\n",
    "  | 0 => 1\n",
    "  | 1 => 1\n",
    "  | n + 2 => F (n + 1) + F n\n",
    "\n",
    "def q (x : ℝ) : ℝ := x + 3\n",
    "\n",
    "\"\"\",\n",
    "\"\"\"example : Injective q := by {}\"\"\"),\n",
    "\n",
    "(\"\"\"import Mathlib.Data.Real.Basic\n",
    "import Mathlib\n",
    "\n",
    "open Function\n",
    " \n",
    "def s (x : ℝ) : ℝ := 5 - x\n",
    "\n",
    "\"\"\",\n",
    "\"\"\"example : s ∘ s = id := by {}\"\"\")\n",
    "]\n",
    "\n",
    "\n",
    "\n",
    "import transformers\n",
    "transformers.set_seed(40)\n",
    "\n",
    "results = {True: [], False: []}\n",
    "for header, theorem in evaluation_theorems:\n",
    "    result = proofsearch.best_first_search(\n",
    "        model, tokenizer, header, theorem, \n",
    "        max_iters=16,\n",
    "        temperatures=[0.5],\n",
    "        num_samples=8,\n",
    "        verbose=True,\n",
    "        prompt_fn=proofsearch.prompt_with_context,\n",
    "        context=header + theorem.replace(\"{}\", \"\"),\n",
    "        path_to_repl=PATH_TO_REPL\n",
    "    )\n",
    "    print(\"Success: %s\" % result['success'])\n",
    "    results[result['success']].append(result)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here are the successfully closed theorems and their generated proofs:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1.000 closed\n",
      "theorem not_superpowered_zero : ¬ Superpowered 0 := by \n",
      "\tintro h\n",
      "\tsimp [Superpowered] at h\n",
      "\texact not_prime_one (h 0)\n",
      "\n",
      "example : Injective q := by \n",
      "\tintro x y h\n",
      "\tsimpa [q] using congr_arg q h\n",
      "\n",
      "example : s ∘ s = id := by \n",
      "\tfunext x\n",
      "\tsimp [s, Function.comp]\n",
      "\n"
     ]
    }
   ],
   "source": [
    "def print_result(result):\n",
    "    print(result['theorem_statement'].replace('{}', '') + '\\n\\t' + '\\n\\t'.join(result['proof']) + '\\n')\n",
    "\n",
    "print(\"%.3f closed\" % (len(results[True])/ (len(results[True])+len(results[False]))))\n",
    "for result in results[True]:\n",
    "    print_result(result)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Next steps\n",
    "\n",
    "In the final notebook, we will incorporate our model into a VS Code tool that generates next-step suggestions with the model, enabling a form of \"human-machine collaboration\". \n",
    "Building a tool is also helpful for thinking about practical requirements (e.g. runtime, generalizing to different projects)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "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
}