From 768f89eff848c2f068d10795fa6ea986cd143b17 Mon Sep 17 00:00:00 2001 From: jsboige Date: Wed, 30 Sep 2026 07:49:03 +0200 Subject: [PATCH] fix(lean,#18453): Lean-05 c.62 -- nom canonique Lean-06 dans source ET sortie (re-exec kernel lean4, contexte lake) Co-Authored-By: Claude Sonnet 5 --- .../Lean/Lean-05-Tactics-Lean.ipynb | 800 ++++++++++-------- 1 file changed, 436 insertions(+), 364 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-05-Tactics-Lean.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-05-Tactics-Lean.ipynb index 4e4993db1e..8ce7de6cc8 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-05-Tactics-Lean.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-05-Tactics-Lean.ipynb @@ -5,10 +5,10 @@ "id": "17bf1bc5", "metadata": { "papermill": { - "duration": 0.005569, - "end_time": "2026-06-07T15:28:10.656184+00:00", + "duration": 0.029623, + "end_time": "2026-09-30T05:45:59.105371+00:00", "exception": false, - "start_time": "2026-06-07T15:28:10.650615+00:00", + "start_time": "2026-09-30T05:45:59.075748+00:00", "status": "completed" }, "tags": [] @@ -63,10 +63,10 @@ "id": "6d822f2b", "metadata": { "papermill": { - "duration": 0.003964, - "end_time": "2026-06-07T15:28:10.664389+00:00", + "duration": 0.024834, + "end_time": "2026-09-30T05:45:59.155583+00:00", "exception": false, - "start_time": "2026-06-07T15:28:10.660425+00:00", + "start_time": "2026-09-30T05:45:59.130749+00:00", "status": "completed" }, "tags": [] @@ -87,16 +87,16 @@ "id": "2d996e6e", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:10.673706Z", - "iopub.status.busy": "2026-06-07T15:28:10.673533Z", - "iopub.status.idle": "2026-06-07T15:28:11.983606Z", - "shell.execute_reply": "2026-06-07T15:28:11.982733Z" + "iopub.execute_input": "2026-09-30T05:45:59.196131Z", + "iopub.status.busy": "2026-09-30T05:45:59.195954Z", + "iopub.status.idle": "2026-09-30T05:47:40.962436Z", + "shell.execute_reply": "2026-09-30T05:47:40.961541Z" }, "papermill": { - "duration": 1.315388, - "end_time": "2026-06-07T15:28:11.984135+00:00", + "duration": 101.802554, + "end_time": "2026-09-30T05:47:40.977429+00:00", "exception": false, - "start_time": "2026-06-07T15:28:10.668747+00:00", + "start_time": "2026-09-30T05:45:59.174875+00:00", "status": "completed" }, "tags": [] @@ -206,10 +206,10 @@ "id": "32371d33", "metadata": { "papermill": { - "duration": 0.0039, - "end_time": "2026-06-07T15:28:11.993158+00:00", + "duration": 0.022595, + "end_time": "2026-09-30T05:47:41.025641+00:00", "exception": false, - "start_time": "2026-06-07T15:28:11.989258+00:00", + "start_time": "2026-09-30T05:47:41.003046+00:00", "status": "completed" }, "tags": [] @@ -234,16 +234,16 @@ "id": "1799fb34", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:12.001699Z", - "iopub.status.busy": "2026-06-07T15:28:12.001542Z", - "iopub.status.idle": "2026-06-07T15:28:12.107749Z", - "shell.execute_reply": "2026-06-07T15:28:12.106935Z" + "iopub.execute_input": "2026-09-30T05:47:41.071258Z", + "iopub.status.busy": "2026-09-30T05:47:41.071070Z", + "iopub.status.idle": "2026-09-30T05:47:41.241566Z", + "shell.execute_reply": "2026-09-30T05:47:41.240659Z" }, "papermill": { - "duration": 0.11157, - "end_time": "2026-06-07T15:28:12.108525+00:00", + "duration": 0.195639, + "end_time": "2026-09-30T05:47:41.242173+00:00", "exception": false, - "start_time": "2026-06-07T15:28:11.996955+00:00", + "start_time": "2026-09-30T05:47:41.046534+00:00", "status": "completed" }, "tags": [] @@ -318,10 +318,10 @@ "id": "3cd3b600", "metadata": { "papermill": { - "duration": 0.003918, - "end_time": "2026-06-07T15:28:12.116650+00:00", + "duration": 0.025834, + "end_time": "2026-09-30T05:47:41.286094+00:00", "exception": false, - "start_time": "2026-06-07T15:28:12.112732+00:00", + "start_time": "2026-09-30T05:47:41.260260+00:00", "status": "completed" }, "tags": [] @@ -346,16 +346,16 @@ "id": "f2e40954", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:12.125363Z", - "iopub.status.busy": "2026-06-07T15:28:12.125223Z", - "iopub.status.idle": "2026-06-07T15:28:12.234591Z", - "shell.execute_reply": "2026-06-07T15:28:12.233514Z" + "iopub.execute_input": "2026-09-30T05:47:41.332605Z", + "iopub.status.busy": "2026-09-30T05:47:41.332414Z", + "iopub.status.idle": "2026-09-30T05:47:41.494176Z", + "shell.execute_reply": "2026-09-30T05:47:41.492819Z" }, "papermill": { - "duration": 0.114603, - "end_time": "2026-06-07T15:28:12.235083+00:00", + "duration": 0.184925, + "end_time": "2026-09-30T05:47:41.495728+00:00", "exception": false, - "start_time": "2026-06-07T15:28:12.120480+00:00", + "start_time": "2026-09-30T05:47:41.310803+00:00", "status": "completed" }, "tags": [] @@ -424,10 +424,10 @@ "id": "caf83a6d", "metadata": { "papermill": { - "duration": 0.004031, - "end_time": "2026-06-07T15:28:12.243145+00:00", + "duration": 0.019895, + "end_time": "2026-09-30T05:47:41.535906+00:00", "exception": false, - "start_time": "2026-06-07T15:28:12.239114+00:00", + "start_time": "2026-09-30T05:47:41.516011+00:00", "status": "completed" }, "tags": [] @@ -452,16 +452,16 @@ "id": "9f814019", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:12.253152Z", - "iopub.status.busy": "2026-06-07T15:28:12.252976Z", - "iopub.status.idle": "2026-06-07T15:28:12.362704Z", - "shell.execute_reply": "2026-06-07T15:28:12.362043Z" + "iopub.execute_input": "2026-09-30T05:47:41.575523Z", + "iopub.status.busy": "2026-09-30T05:47:41.575339Z", + "iopub.status.idle": "2026-09-30T05:47:41.737698Z", + "shell.execute_reply": "2026-09-30T05:47:41.736480Z" }, "papermill": { - "duration": 0.115568, - "end_time": "2026-06-07T15:28:12.363234+00:00", + "duration": 0.185092, + "end_time": "2026-09-30T05:47:41.738469+00:00", "exception": false, - "start_time": "2026-06-07T15:28:12.247666+00:00", + "start_time": "2026-09-30T05:47:41.553377+00:00", "status": "completed" }, "tags": [] @@ -557,10 +557,10 @@ "id": "bd153878", "metadata": { "papermill": { - "duration": 0.003837, - "end_time": "2026-06-07T15:28:12.371282+00:00", + "duration": 0.028898, + "end_time": "2026-09-30T05:47:41.789843+00:00", "exception": false, - "start_time": "2026-06-07T15:28:12.367445+00:00", + "start_time": "2026-09-30T05:47:41.760945+00:00", "status": "completed" }, "tags": [] @@ -583,16 +583,16 @@ "id": "45ee591b", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:12.380615Z", - "iopub.status.busy": "2026-06-07T15:28:12.380470Z", - "iopub.status.idle": "2026-06-07T15:28:12.488136Z", - "shell.execute_reply": "2026-06-07T15:28:12.487109Z" + "iopub.execute_input": "2026-09-30T05:47:41.846651Z", + "iopub.status.busy": "2026-09-30T05:47:41.846466Z", + "iopub.status.idle": "2026-09-30T05:47:42.001552Z", + "shell.execute_reply": "2026-09-30T05:47:42.000547Z" }, "papermill": { - "duration": 0.113668, - "end_time": "2026-06-07T15:28:12.488734+00:00", + "duration": 0.190319, + "end_time": "2026-09-30T05:47:42.002719+00:00", "exception": false, - "start_time": "2026-06-07T15:28:12.375066+00:00", + "start_time": "2026-09-30T05:47:41.812400+00:00", "status": "completed" }, "tags": [] @@ -682,10 +682,10 @@ "id": "1fcbf065", "metadata": { "papermill": { - "duration": 0.008055, - "end_time": "2026-06-07T15:28:12.501271+00:00", + "duration": 0.020336, + "end_time": "2026-09-30T05:47:42.043234+00:00", "exception": false, - "start_time": "2026-06-07T15:28:12.493216+00:00", + "start_time": "2026-09-30T05:47:42.022898+00:00", "status": "completed" }, "tags": [] @@ -708,16 +708,16 @@ "id": "63cdc226", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:12.510470Z", - "iopub.status.busy": "2026-06-07T15:28:12.510324Z", - "iopub.status.idle": "2026-06-07T15:28:12.618749Z", - "shell.execute_reply": "2026-06-07T15:28:12.617805Z" + "iopub.execute_input": "2026-09-30T05:47:42.097822Z", + "iopub.status.busy": "2026-09-30T05:47:42.097641Z", + "iopub.status.idle": "2026-09-30T05:47:42.255244Z", + "shell.execute_reply": "2026-09-30T05:47:42.253874Z" }, "papermill": { - "duration": 0.113667, - "end_time": "2026-06-07T15:28:12.619274+00:00", + "duration": 0.188994, + "end_time": "2026-09-30T05:47:42.255962+00:00", "exception": false, - "start_time": "2026-06-07T15:28:12.505607+00:00", + "start_time": "2026-09-30T05:47:42.066968+00:00", "status": "completed" }, "tags": [] @@ -736,7 +736,10 @@ " \n", "
\n", " 
-- assumption trouve automatiquement l'hypothese
\n", - "
🟨 unused variable `hq`\n",
+       "
🟨 Variable name `hq` is not explicitly referenced.\n",
+       "\n",
+       "Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\n",
+       "  [apply] _hq\n",
        "\n",
        "Note: This linter can be disabled with `set_option linter.unusedVariables false`
\n",
        "
  assumption   -- Trouve hp : p dans le contexte
\n",
@@ -760,7 +763,7 @@
        "   \"pos\": {\"line\": 2, \"column\": 50},\r\n",
        "   \"endPos\": {\"line\": 2, \"column\": 52},\r\n",
        "   \"data\":\r\n",
-       "   \"unused variable `hq`\\n\\nNote: This linter can be disabled with `set_option linter.unusedVariables false`\"}],\r\n",
+       "   \"Variable name `hq` is not explicitly referenced.\\n\\nHint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\\n  [apply] _hq\\n\\nNote: This linter can be disabled with `set_option linter.unusedVariables false`\"}],\r\n",
        " \"env\": 5}\n",
        "        \n",
        "    "
@@ -768,7 +771,10 @@
       "text/plain": [
        "-- assumption trouve automatiquement l'hypothese\n",
        "theorem assumption_example (p q : Prop) (hp : p) (hq : q) : p := by\n",
-       "                                                  ──▶ 🟨 unused variable `hq`\n",
+       "                                                  ──▶ 🟨 Variable name `hq` is not explicitly referenced.\n",
+       "\n",
+       "Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\n",
+       "  [apply] _hq\n",
        "\n",
        "Note: This linter can be disabled with `set_option linter.unusedVariables false`\n",
        "  assumption   -- Trouve hp : p dans le contexte\n",
@@ -789,7 +795,7 @@
        "   \"pos\": {\"line\": 2, \"column\": 50},\r\n",
        "   \"endPos\": {\"line\": 2, \"column\": 52},\r\n",
        "   \"data\":\r\n",
-       "   \"unused variable `hq`\\n\\nNote: This linter can be disabled with `set_option linter.unusedVariables false`\"}],\r\n",
+       "   \"Variable name `hq` is not explicitly referenced.\\n\\nHint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\\n  [apply] _hq\\n\\nNote: This linter can be disabled with `set_option linter.unusedVariables false`\"}],\r\n",
        " \"env\": 5}"
       ]
      },
@@ -815,10 +821,10 @@
    "id": "405db572",
    "metadata": {
     "papermill": {
-     "duration": 0.00411,
-     "end_time": "2026-06-07T15:28:12.627885+00:00",
+     "duration": 0.023405,
+     "end_time": "2026-09-30T05:47:42.323520+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:12.623775+00:00",
+     "start_time": "2026-09-30T05:47:42.300115+00:00",
      "status": "completed"
     },
     "tags": []
@@ -841,16 +847,16 @@
    "id": "f5244c6a",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:12.636987Z",
-     "iopub.status.busy": "2026-06-07T15:28:12.636853Z",
-     "iopub.status.idle": "2026-06-07T15:28:12.748256Z",
-     "shell.execute_reply": "2026-06-07T15:28:12.747406Z"
+     "iopub.execute_input": "2026-09-30T05:47:42.377023Z",
+     "iopub.status.busy": "2026-09-30T05:47:42.376834Z",
+     "iopub.status.idle": "2026-09-30T05:47:42.543322Z",
+     "shell.execute_reply": "2026-09-30T05:47:42.542260Z"
     },
     "papermill": {
-     "duration": 0.116597,
-     "end_time": "2026-06-07T15:28:12.748720+00:00",
+     "duration": 0.194774,
+     "end_time": "2026-09-30T05:47:42.544372+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:12.632123+00:00",
+     "start_time": "2026-09-30T05:47:42.349598+00:00",
      "status": "completed"
     },
     "tags": []
@@ -922,10 +928,10 @@
    "id": "74e9802f",
    "metadata": {
     "papermill": {
-     "duration": 0.004176,
-     "end_time": "2026-06-07T15:28:12.757446+00:00",
+     "duration": 0.023474,
+     "end_time": "2026-09-30T05:47:42.590405+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:12.753270+00:00",
+     "start_time": "2026-09-30T05:47:42.566931+00:00",
      "status": "completed"
     },
     "tags": []
@@ -942,16 +948,16 @@
    "id": "c937eb84",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:12.766541Z",
-     "iopub.status.busy": "2026-06-07T15:28:12.766403Z",
-     "iopub.status.idle": "2026-06-07T15:28:12.877395Z",
-     "shell.execute_reply": "2026-06-07T15:28:12.876547Z"
+     "iopub.execute_input": "2026-09-30T05:47:42.638157Z",
+     "iopub.status.busy": "2026-09-30T05:47:42.637961Z",
+     "iopub.status.idle": "2026-09-30T05:47:42.799607Z",
+     "shell.execute_reply": "2026-09-30T05:47:42.797989Z"
     },
     "papermill": {
-     "duration": 0.116392,
-     "end_time": "2026-06-07T15:28:12.878121+00:00",
+     "duration": 0.191264,
+     "end_time": "2026-09-30T05:47:42.800565+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:12.761729+00:00",
+     "start_time": "2026-09-30T05:47:42.609301+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1041,10 +1047,10 @@
    "id": "6f2ac925",
    "metadata": {
     "papermill": {
-     "duration": 0.004808,
-     "end_time": "2026-06-07T15:28:12.888049+00:00",
+     "duration": 0.019657,
+     "end_time": "2026-09-30T05:47:42.843985+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:12.883241+00:00",
+     "start_time": "2026-09-30T05:47:42.824328+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1067,16 +1073,16 @@
    "id": "f6ad0774",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:12.898686Z",
-     "iopub.status.busy": "2026-06-07T15:28:12.898524Z",
-     "iopub.status.idle": "2026-06-07T15:28:13.024873Z",
-     "shell.execute_reply": "2026-06-07T15:28:13.024139Z"
+     "iopub.execute_input": "2026-09-30T05:47:42.889125Z",
+     "iopub.status.busy": "2026-09-30T05:47:42.888813Z",
+     "iopub.status.idle": "2026-09-30T05:47:43.080999Z",
+     "shell.execute_reply": "2026-09-30T05:47:43.079553Z"
     },
     "papermill": {
-     "duration": 0.132792,
-     "end_time": "2026-06-07T15:28:13.025781+00:00",
+     "duration": 0.216406,
+     "end_time": "2026-09-30T05:47:43.081705+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:12.892989+00:00",
+     "start_time": "2026-09-30T05:47:42.865299+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1163,10 +1169,10 @@
    "id": "51847327",
    "metadata": {
     "papermill": {
-     "duration": 0.005053,
-     "end_time": "2026-06-07T15:28:13.035683+00:00",
+     "duration": 0.021116,
+     "end_time": "2026-09-30T05:47:43.125878+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.030630+00:00",
+     "start_time": "2026-09-30T05:47:43.104762+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1183,16 +1189,16 @@
    "id": "d7673f0c",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:13.046125Z",
-     "iopub.status.busy": "2026-06-07T15:28:13.045939Z",
-     "iopub.status.idle": "2026-06-07T15:28:13.152508Z",
-     "shell.execute_reply": "2026-06-07T15:28:13.151760Z"
+     "iopub.execute_input": "2026-09-30T05:47:43.169828Z",
+     "iopub.status.busy": "2026-09-30T05:47:43.169640Z",
+     "iopub.status.idle": "2026-09-30T05:47:43.328929Z",
+     "shell.execute_reply": "2026-09-30T05:47:43.327840Z"
     },
     "papermill": {
-     "duration": 0.112548,
-     "end_time": "2026-06-07T15:28:13.153013+00:00",
+     "duration": 0.182274,
+     "end_time": "2026-09-30T05:47:43.329736+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.040465+00:00",
+     "start_time": "2026-09-30T05:47:43.147462+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1264,10 +1270,10 @@
    "id": "bb7bc147",
    "metadata": {
     "papermill": {
-     "duration": 0.004201,
-     "end_time": "2026-06-07T15:28:13.161915+00:00",
+     "duration": 0.022469,
+     "end_time": "2026-09-30T05:47:43.373092+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.157714+00:00",
+     "start_time": "2026-09-30T05:47:43.350623+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1284,16 +1290,16 @@
    "id": "7b22e015",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:13.171214Z",
-     "iopub.status.busy": "2026-06-07T15:28:13.171081Z",
-     "iopub.status.idle": "2026-06-07T15:28:13.280495Z",
-     "shell.execute_reply": "2026-06-07T15:28:13.279775Z"
+     "iopub.execute_input": "2026-09-30T05:47:43.427493Z",
+     "iopub.status.busy": "2026-09-30T05:47:43.427221Z",
+     "iopub.status.idle": "2026-09-30T05:47:43.603870Z",
+     "shell.execute_reply": "2026-09-30T05:47:43.602338Z"
     },
     "papermill": {
-     "duration": 0.11488,
-     "end_time": "2026-06-07T15:28:13.281011+00:00",
+     "duration": 0.20247,
+     "end_time": "2026-09-30T05:47:43.605354+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.166131+00:00",
+     "start_time": "2026-09-30T05:47:43.402884+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1365,10 +1371,10 @@
    "id": "74f93458",
    "metadata": {
     "papermill": {
-     "duration": 0.004361,
-     "end_time": "2026-06-07T15:28:13.290206+00:00",
+     "duration": 0.022067,
+     "end_time": "2026-09-30T05:47:43.654926+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.285845+00:00",
+     "start_time": "2026-09-30T05:47:43.632859+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1400,16 +1406,16 @@
    "id": "d116e2e1",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:13.301845Z",
-     "iopub.status.busy": "2026-06-07T15:28:13.301697Z",
-     "iopub.status.idle": "2026-06-07T15:28:13.416873Z",
-     "shell.execute_reply": "2026-06-07T15:28:13.416331Z"
+     "iopub.execute_input": "2026-09-30T05:47:43.711687Z",
+     "iopub.status.busy": "2026-09-30T05:47:43.711482Z",
+     "iopub.status.idle": "2026-09-30T05:47:43.875917Z",
+     "shell.execute_reply": "2026-09-30T05:47:43.874944Z"
     },
     "papermill": {
-     "duration": 0.122243,
-     "end_time": "2026-06-07T15:28:13.417310+00:00",
+     "duration": 0.197471,
+     "end_time": "2026-09-30T05:47:43.876870+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.295067+00:00",
+     "start_time": "2026-09-30T05:47:43.679399+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1529,10 +1535,10 @@
    "id": "b70a5584",
    "metadata": {
     "papermill": {
-     "duration": 0.004715,
-     "end_time": "2026-06-07T15:28:13.427015+00:00",
+     "duration": 0.023651,
+     "end_time": "2026-09-30T05:47:43.925068+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.422300+00:00",
+     "start_time": "2026-09-30T05:47:43.901417+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1549,16 +1555,16 @@
    "id": "db139759",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:13.438879Z",
-     "iopub.status.busy": "2026-06-07T15:28:13.438706Z",
-     "iopub.status.idle": "2026-06-07T15:28:13.553483Z",
-     "shell.execute_reply": "2026-06-07T15:28:13.552697Z"
+     "iopub.execute_input": "2026-09-30T05:47:43.969968Z",
+     "iopub.status.busy": "2026-09-30T05:47:43.969792Z",
+     "iopub.status.idle": "2026-09-30T05:47:44.144000Z",
+     "shell.execute_reply": "2026-09-30T05:47:44.142975Z"
     },
     "papermill": {
-     "duration": 0.121056,
-     "end_time": "2026-06-07T15:28:13.554029+00:00",
+     "duration": 0.19809,
+     "end_time": "2026-09-30T05:47:44.144579+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.432973+00:00",
+     "start_time": "2026-09-30T05:47:43.946489+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1660,10 +1666,10 @@
    "id": "a4f14a25",
    "metadata": {
     "papermill": {
-     "duration": 0.004775,
-     "end_time": "2026-06-07T15:28:13.563997+00:00",
+     "duration": 0.050593,
+     "end_time": "2026-09-30T05:47:44.234881+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.559222+00:00",
+     "start_time": "2026-09-30T05:47:44.184288+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1680,16 +1686,16 @@
    "id": "18307adc",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:13.575082Z",
-     "iopub.status.busy": "2026-06-07T15:28:13.574927Z",
-     "iopub.status.idle": "2026-06-07T15:28:13.684030Z",
-     "shell.execute_reply": "2026-06-07T15:28:13.683425Z"
+     "iopub.execute_input": "2026-09-30T05:47:44.318102Z",
+     "iopub.status.busy": "2026-09-30T05:47:44.317913Z",
+     "iopub.status.idle": "2026-09-30T05:47:44.475117Z",
+     "shell.execute_reply": "2026-09-30T05:47:44.474211Z"
     },
     "papermill": {
-     "duration": 0.115768,
-     "end_time": "2026-06-07T15:28:13.684538+00:00",
+     "duration": 0.204317,
+     "end_time": "2026-09-30T05:47:44.475696+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.568770+00:00",
+     "start_time": "2026-09-30T05:47:44.271379+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1764,10 +1770,10 @@
    "id": "58e75458",
    "metadata": {
     "papermill": {
-     "duration": 0.00462,
-     "end_time": "2026-06-07T15:28:13.694354+00:00",
+     "duration": 0.030571,
+     "end_time": "2026-09-30T05:47:44.527338+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.689734+00:00",
+     "start_time": "2026-09-30T05:47:44.496767+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1784,16 +1790,16 @@
    "id": "81c6424d",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:13.719039Z",
-     "iopub.status.busy": "2026-06-07T15:28:13.718894Z",
-     "iopub.status.idle": "2026-06-07T15:28:13.827584Z",
-     "shell.execute_reply": "2026-06-07T15:28:13.826499Z"
+     "iopub.execute_input": "2026-09-30T05:47:44.590672Z",
+     "iopub.status.busy": "2026-09-30T05:47:44.590481Z",
+     "iopub.status.idle": "2026-09-30T05:47:44.748823Z",
+     "shell.execute_reply": "2026-09-30T05:47:44.747810Z"
     },
     "papermill": {
-     "duration": 0.129441,
-     "end_time": "2026-06-07T15:28:13.828392+00:00",
+     "duration": 0.186625,
+     "end_time": "2026-09-30T05:47:44.749438+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.698951+00:00",
+     "start_time": "2026-09-30T05:47:44.562813+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1865,10 +1871,10 @@
    "id": "68918a35",
    "metadata": {
     "papermill": {
-     "duration": 0.005876,
-     "end_time": "2026-06-07T15:28:13.840346+00:00",
+     "duration": 0.022404,
+     "end_time": "2026-09-30T05:47:44.794340+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.834470+00:00",
+     "start_time": "2026-09-30T05:47:44.771936+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1893,16 +1899,16 @@
    "id": "36816a73",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:13.851854Z",
-     "iopub.status.busy": "2026-06-07T15:28:13.851698Z",
-     "iopub.status.idle": "2026-06-07T15:28:13.967830Z",
-     "shell.execute_reply": "2026-06-07T15:28:13.967110Z"
+     "iopub.execute_input": "2026-09-30T05:47:44.838515Z",
+     "iopub.status.busy": "2026-09-30T05:47:44.838329Z",
+     "iopub.status.idle": "2026-09-30T05:47:45.004318Z",
+     "shell.execute_reply": "2026-09-30T05:47:45.003452Z"
     },
     "papermill": {
-     "duration": 0.122416,
-     "end_time": "2026-06-07T15:28:13.968335+00:00",
+     "duration": 0.187519,
+     "end_time": "2026-09-30T05:47:45.004842+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.845919+00:00",
+     "start_time": "2026-09-30T05:47:44.817323+00:00",
      "status": "completed"
     },
     "tags": []
@@ -1986,10 +1992,10 @@
    "id": "44cb4396",
    "metadata": {
     "papermill": {
-     "duration": 0.005328,
-     "end_time": "2026-06-07T15:28:13.978822+00:00",
+     "duration": 0.022252,
+     "end_time": "2026-09-30T05:47:45.046100+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.973494+00:00",
+     "start_time": "2026-09-30T05:47:45.023848+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2006,16 +2012,16 @@
    "id": "182cdbc9",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:13.990555Z",
-     "iopub.status.busy": "2026-06-07T15:28:13.990392Z",
-     "iopub.status.idle": "2026-06-07T15:28:14.111525Z",
-     "shell.execute_reply": "2026-06-07T15:28:14.110877Z"
+     "iopub.execute_input": "2026-09-30T05:47:45.093764Z",
+     "iopub.status.busy": "2026-09-30T05:47:45.093473Z",
+     "iopub.status.idle": "2026-09-30T05:47:45.261728Z",
+     "shell.execute_reply": "2026-09-30T05:47:45.260808Z"
     },
     "papermill": {
-     "duration": 0.127982,
-     "end_time": "2026-06-07T15:28:14.112059+00:00",
+     "duration": 0.194643,
+     "end_time": "2026-09-30T05:47:45.262280+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:13.984077+00:00",
+     "start_time": "2026-09-30T05:47:45.067637+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2102,10 +2108,10 @@
    "id": "875f866e",
    "metadata": {
     "papermill": {
-     "duration": 0.005089,
-     "end_time": "2026-06-07T15:28:14.122659+00:00",
+     "duration": 0.029199,
+     "end_time": "2026-09-30T05:47:45.317761+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.117570+00:00",
+     "start_time": "2026-09-30T05:47:45.288562+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2132,16 +2138,16 @@
    "id": "6eeec3ad",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:14.133297Z",
-     "iopub.status.busy": "2026-06-07T15:28:14.133180Z",
-     "iopub.status.idle": "2026-06-07T15:28:14.250003Z",
-     "shell.execute_reply": "2026-06-07T15:28:14.249096Z"
+     "iopub.execute_input": "2026-09-30T05:47:45.364633Z",
+     "iopub.status.busy": "2026-09-30T05:47:45.364423Z",
+     "iopub.status.idle": "2026-09-30T05:47:45.523072Z",
+     "shell.execute_reply": "2026-09-30T05:47:45.522143Z"
     },
     "papermill": {
-     "duration": 0.12349,
-     "end_time": "2026-06-07T15:28:14.250889+00:00",
+     "duration": 0.183556,
+     "end_time": "2026-09-30T05:47:45.523896+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.127399+00:00",
+     "start_time": "2026-09-30T05:47:45.340340+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2219,10 +2225,10 @@
    "id": "589d7c21",
    "metadata": {
     "papermill": {
-     "duration": 0.004923,
-     "end_time": "2026-06-07T15:28:14.261093+00:00",
+     "duration": 0.033035,
+     "end_time": "2026-09-30T05:47:45.581001+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.256170+00:00",
+     "start_time": "2026-09-30T05:47:45.547966+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2247,16 +2253,16 @@
    "id": "1c8cf1a6",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:14.274807Z",
-     "iopub.status.busy": "2026-06-07T15:28:14.274676Z",
-     "iopub.status.idle": "2026-06-07T15:28:14.391422Z",
-     "shell.execute_reply": "2026-06-07T15:28:14.390743Z"
+     "iopub.execute_input": "2026-09-30T05:47:45.627594Z",
+     "iopub.status.busy": "2026-09-30T05:47:45.627416Z",
+     "iopub.status.idle": "2026-09-30T05:47:45.792915Z",
+     "shell.execute_reply": "2026-09-30T05:47:45.792035Z"
     },
     "papermill": {
-     "duration": 0.125967,
-     "end_time": "2026-06-07T15:28:14.391911+00:00",
+     "duration": 0.185471,
+     "end_time": "2026-09-30T05:47:45.793846+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.265944+00:00",
+     "start_time": "2026-09-30T05:47:45.608375+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2337,10 +2343,10 @@
    "id": "aea953de",
    "metadata": {
     "papermill": {
-     "duration": 0.005175,
-     "end_time": "2026-06-07T15:28:14.402347+00:00",
+     "duration": 0.029291,
+     "end_time": "2026-09-30T05:47:45.845751+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.397172+00:00",
+     "start_time": "2026-09-30T05:47:45.816460+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2376,16 +2382,16 @@
    "id": "e00b63d2",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:14.412787Z",
-     "iopub.status.busy": "2026-06-07T15:28:14.412666Z",
-     "iopub.status.idle": "2026-06-07T15:28:14.528203Z",
-     "shell.execute_reply": "2026-06-07T15:28:14.527234Z"
+     "iopub.execute_input": "2026-09-30T05:47:45.900279Z",
+     "iopub.status.busy": "2026-09-30T05:47:45.900079Z",
+     "iopub.status.idle": "2026-09-30T05:47:46.068476Z",
+     "shell.execute_reply": "2026-09-30T05:47:46.067574Z"
     },
     "papermill": {
-     "duration": 0.121474,
-     "end_time": "2026-06-07T15:28:14.528657+00:00",
+     "duration": 0.192608,
+     "end_time": "2026-09-30T05:47:46.069214+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.407183+00:00",
+     "start_time": "2026-09-30T05:47:45.876606+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2469,10 +2475,10 @@
    "id": "64af1a30",
    "metadata": {
     "papermill": {
-     "duration": 0.005554,
-     "end_time": "2026-06-07T15:28:14.539884+00:00",
+     "duration": 0.024489,
+     "end_time": "2026-09-30T05:47:46.118501+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.534330+00:00",
+     "start_time": "2026-09-30T05:47:46.094012+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2520,16 +2526,16 @@
    "id": "497820cf",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:14.551653Z",
-     "iopub.status.busy": "2026-06-07T15:28:14.551418Z",
-     "iopub.status.idle": "2026-06-07T15:28:14.662274Z",
-     "shell.execute_reply": "2026-06-07T15:28:14.661417Z"
+     "iopub.execute_input": "2026-09-30T05:47:46.166872Z",
+     "iopub.status.busy": "2026-09-30T05:47:46.166664Z",
+     "iopub.status.idle": "2026-09-30T05:47:46.322336Z",
+     "shell.execute_reply": "2026-09-30T05:47:46.321421Z"
     },
     "papermill": {
-     "duration": 0.117505,
-     "end_time": "2026-06-07T15:28:14.662852+00:00",
+     "duration": 0.183494,
+     "end_time": "2026-09-30T05:47:46.323287+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.545347+00:00",
+     "start_time": "2026-09-30T05:47:46.139793+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2598,10 +2604,10 @@
    "id": "1d2a77dd",
    "metadata": {
     "papermill": {
-     "duration": 0.00542,
-     "end_time": "2026-06-07T15:28:14.673884+00:00",
+     "duration": 0.050903,
+     "end_time": "2026-09-30T05:47:46.416134+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.668464+00:00",
+     "start_time": "2026-09-30T05:47:46.365231+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2630,16 +2636,16 @@
    "id": "eb55cf94",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:14.684980Z",
-     "iopub.status.busy": "2026-06-07T15:28:14.684851Z",
-     "iopub.status.idle": "2026-06-07T15:28:14.793256Z",
-     "shell.execute_reply": "2026-06-07T15:28:14.792466Z"
+     "iopub.execute_input": "2026-09-30T05:47:46.479290Z",
+     "iopub.status.busy": "2026-09-30T05:47:46.479097Z",
+     "iopub.status.idle": "2026-09-30T05:47:46.636159Z",
+     "shell.execute_reply": "2026-09-30T05:47:46.635475Z"
     },
     "papermill": {
-     "duration": 0.114822,
-     "end_time": "2026-06-07T15:28:14.793838+00:00",
+     "duration": 0.188639,
+     "end_time": "2026-09-30T05:47:46.637022+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.679016+00:00",
+     "start_time": "2026-09-30T05:47:46.448383+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2710,6 +2716,13 @@
    "cell_type": "markdown",
    "id": "b7441001",
    "metadata": {
+    "papermill": {
+     "duration": 0.023528,
+     "end_time": "2026-09-30T05:47:46.682902+00:00",
+     "exception": false,
+     "start_time": "2026-09-30T05:47:46.659374+00:00",
+     "status": "completed"
+    },
     "tags": []
    },
    "source": [
@@ -2721,10 +2734,10 @@
    "id": "81603479",
    "metadata": {
     "papermill": {
-     "duration": 0.005778,
-     "end_time": "2026-06-07T15:28:14.805542+00:00",
+     "duration": 0.026928,
+     "end_time": "2026-09-30T05:47:46.733762+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.799764+00:00",
+     "start_time": "2026-09-30T05:47:46.706834+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2763,16 +2776,16 @@
    "id": "cefe9134",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:14.817347Z",
-     "iopub.status.busy": "2026-06-07T15:28:14.817205Z",
-     "iopub.status.idle": "2026-06-07T15:28:14.926486Z",
-     "shell.execute_reply": "2026-06-07T15:28:14.925941Z"
+     "iopub.execute_input": "2026-09-30T05:47:46.787305Z",
+     "iopub.status.busy": "2026-09-30T05:47:46.787112Z",
+     "iopub.status.idle": "2026-09-30T05:47:46.939796Z",
+     "shell.execute_reply": "2026-09-30T05:47:46.938965Z"
     },
     "papermill": {
-     "duration": 0.115964,
-     "end_time": "2026-06-07T15:28:14.927166+00:00",
+     "duration": 0.176313,
+     "end_time": "2026-09-30T05:47:46.940432+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.811202+00:00",
+     "start_time": "2026-09-30T05:47:46.764119+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2849,6 +2862,13 @@
    "cell_type": "markdown",
    "id": "b7461002",
    "metadata": {
+    "papermill": {
+     "duration": 0.03244,
+     "end_time": "2026-09-30T05:47:47.000909+00:00",
+     "exception": false,
+     "start_time": "2026-09-30T05:47:46.968469+00:00",
+     "status": "completed"
+    },
     "tags": []
    },
    "source": [
@@ -2860,10 +2880,10 @@
    "id": "8b56cefe",
    "metadata": {
     "papermill": {
-     "duration": 0.005125,
-     "end_time": "2026-06-07T15:28:14.938230+00:00",
+     "duration": 0.024334,
+     "end_time": "2026-09-30T05:47:47.053324+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.933105+00:00",
+     "start_time": "2026-09-30T05:47:47.028990+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2892,16 +2912,16 @@
    "id": "abd55f74",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:14.949419Z",
-     "iopub.status.busy": "2026-06-07T15:28:14.949286Z",
-     "iopub.status.idle": "2026-06-07T15:28:15.060168Z",
-     "shell.execute_reply": "2026-06-07T15:28:15.059349Z"
+     "iopub.execute_input": "2026-09-30T05:47:47.101457Z",
+     "iopub.status.busy": "2026-09-30T05:47:47.101162Z",
+     "iopub.status.idle": "2026-09-30T05:47:47.265307Z",
+     "shell.execute_reply": "2026-09-30T05:47:47.264384Z"
     },
     "papermill": {
-     "duration": 0.117524,
-     "end_time": "2026-06-07T15:28:15.060850+00:00",
+     "duration": 0.188824,
+     "end_time": "2026-09-30T05:47:47.266286+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:14.943326+00:00",
+     "start_time": "2026-09-30T05:47:47.077462+00:00",
      "status": "completed"
     },
     "tags": []
@@ -2984,6 +3004,13 @@
    "cell_type": "markdown",
    "id": "b7481003",
    "metadata": {
+    "papermill": {
+     "duration": 0.036882,
+     "end_time": "2026-09-30T05:47:47.333634+00:00",
+     "exception": false,
+     "start_time": "2026-09-30T05:47:47.296752+00:00",
+     "status": "completed"
+    },
     "tags": []
    },
    "source": [
@@ -3000,10 +3027,10 @@
    "id": "63c6176f",
    "metadata": {
     "papermill": {
-     "duration": 0.005976,
-     "end_time": "2026-06-07T15:28:15.073210+00:00",
+     "duration": 0.035809,
+     "end_time": "2026-09-30T05:47:47.407782+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:15.067234+00:00",
+     "start_time": "2026-09-30T05:47:47.371973+00:00",
      "status": "completed"
     },
     "tags": []
@@ -3050,16 +3077,16 @@
    "id": "e4ca8a52",
    "metadata": {
     "execution": {
-     "iopub.execute_input": "2026-06-07T15:28:15.087100Z",
-     "iopub.status.busy": "2026-06-07T15:28:15.086943Z",
-     "iopub.status.idle": "2026-06-07T15:28:15.202882Z",
-     "shell.execute_reply": "2026-06-07T15:28:15.201833Z"
+     "iopub.execute_input": "2026-09-30T05:47:47.463198Z",
+     "iopub.status.busy": "2026-09-30T05:47:47.463007Z",
+     "iopub.status.idle": "2026-09-30T05:47:47.627565Z",
+     "shell.execute_reply": "2026-09-30T05:47:47.626908Z"
     },
     "papermill": {
-     "duration": 0.124178,
-     "end_time": "2026-06-07T15:28:15.203409+00:00",
+     "duration": 0.192422,
+     "end_time": "2026-09-30T05:47:47.628187+00:00",
      "exception": false,
-     "start_time": "2026-06-07T15:28:15.079231+00:00",
+     "start_time": "2026-09-30T05:47:47.435765+00:00",
      "status": "completed"
     },
     "tags": []
@@ -3095,7 +3122,7 @@
        "  ih\n",
        "\n",
        "Hint: Omit it from the simp argument list.\n",
-       "  simp ̵[̵i̵h̵]̵\n",
+       "  [apply] simp\n",
        "\n",
        "Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
\n", "
--% env 24
\n", @@ -3111,7 +3138,7 @@ " \"pos\": {\"line\": 15, \"column\": 23},\r\n", " \"endPos\": {\"line\": 15, \"column\": 25},\r\n", " \"data\":\r\n", - " \"This simp argument is unused:\\n ih\\n\\nHint: Omit it from the simp argument list.\\n simp ̵[̵i̵h̵]̵\\n\\nNote: This linter can be disabled with `set_option linter.unusedSimpArgs false`\"}],\r\n", + " \"This simp argument is unused:\\n ih\\n\\nHint: Omit it from the simp argument list.\\n [apply] simp\\n\\nNote: This linter can be disabled with `set_option linter.unusedSimpArgs false`\"}],\r\n", " \"env\": 24}\n", " \n", " " @@ -3136,7 +3163,7 @@ " ih\n", "\n", "Hint: Omit it from the simp argument list.\n", - " simp ̵[̵i̵h̵]̵\n", + " [apply] simp\n", "\n", "Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`\n", "--% env 24\n", @@ -3149,7 +3176,7 @@ " \"pos\": {\"line\": 15, \"column\": 23},\r\n", " \"endPos\": {\"line\": 15, \"column\": 25},\r\n", " \"data\":\r\n", - " \"This simp argument is unused:\\n ih\\n\\nHint: Omit it from the simp argument list.\\n simp ̵[̵i̵h̵]̵\\n\\nNote: This linter can be disabled with `set_option linter.unusedSimpArgs false`\"}],\r\n", + " \"This simp argument is unused:\\n ih\\n\\nHint: Omit it from the simp argument list.\\n [apply] simp\\n\\nNote: This linter can be disabled with `set_option linter.unusedSimpArgs false`\"}],\r\n", " \"env\": 24}" ] }, @@ -3179,6 +3206,13 @@ "cell_type": "markdown", "id": "b7501004", "metadata": { + "papermill": { + "duration": 0.034169, + "end_time": "2026-09-30T05:47:47.694547+00:00", + "exception": false, + "start_time": "2026-09-30T05:47:47.660378+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -3190,10 +3224,10 @@ "id": "edb2e20d", "metadata": { "papermill": { - "duration": 0.00623, - "end_time": "2026-06-07T15:28:15.216142+00:00", + "duration": 0.022695, + "end_time": "2026-09-30T05:47:47.741106+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.209912+00:00", + "start_time": "2026-09-30T05:47:47.718411+00:00", "status": "completed" }, "tags": [] @@ -3232,16 +3266,16 @@ "id": "a53ec84b", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:15.229345Z", - "iopub.status.busy": "2026-06-07T15:28:15.229197Z", - "iopub.status.idle": "2026-06-07T15:28:15.343825Z", - "shell.execute_reply": "2026-06-07T15:28:15.342953Z" + "iopub.execute_input": "2026-09-30T05:47:47.791378Z", + "iopub.status.busy": "2026-09-30T05:47:47.791197Z", + "iopub.status.idle": "2026-09-30T05:47:47.948214Z", + "shell.execute_reply": "2026-09-30T05:47:47.947153Z" }, "papermill": { - "duration": 0.121969, - "end_time": "2026-06-07T15:28:15.344405+00:00", + "duration": 0.182941, + "end_time": "2026-09-30T05:47:47.948904+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.222436+00:00", + "start_time": "2026-09-30T05:47:47.765963+00:00", "status": "completed" }, "tags": [] @@ -3315,6 +3349,13 @@ "cell_type": "markdown", "id": "b7521005", "metadata": { + "papermill": { + "duration": 0.024462, + "end_time": "2026-09-30T05:47:47.996912+00:00", + "exception": false, + "start_time": "2026-09-30T05:47:47.972450+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -3326,10 +3367,10 @@ "id": "636978fd", "metadata": { "papermill": { - "duration": 0.006495, - "end_time": "2026-06-07T15:28:15.357567+00:00", + "duration": 0.0262, + "end_time": "2026-09-30T05:47:48.048082+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.351072+00:00", + "start_time": "2026-09-30T05:47:48.021882+00:00", "status": "completed" }, "tags": [] @@ -3371,16 +3412,16 @@ "id": "9f0f0026", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:15.370373Z", - "iopub.status.busy": "2026-06-07T15:28:15.370230Z", - "iopub.status.idle": "2026-06-07T15:28:15.501736Z", - "shell.execute_reply": "2026-06-07T15:28:15.501128Z" + "iopub.execute_input": "2026-09-30T05:47:48.105973Z", + "iopub.status.busy": "2026-09-30T05:47:48.105788Z", + "iopub.status.idle": "2026-09-30T05:47:48.288353Z", + "shell.execute_reply": "2026-09-30T05:47:48.287278Z" }, "papermill": { - "duration": 0.138327, - "end_time": "2026-06-07T15:28:15.502227+00:00", + "duration": 0.209919, + "end_time": "2026-09-30T05:47:48.288961+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.363900+00:00", + "start_time": "2026-09-30T05:47:48.079042+00:00", "status": "completed" }, "tags": [] @@ -3451,6 +3492,13 @@ "cell_type": "markdown", "id": "b7541006", "metadata": { + "papermill": { + "duration": 0.026748, + "end_time": "2026-09-30T05:47:48.345828+00:00", + "exception": false, + "start_time": "2026-09-30T05:47:48.319080+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -3462,10 +3510,10 @@ "id": "0de421f5", "metadata": { "papermill": { - "duration": 0.006571, - "end_time": "2026-06-07T15:28:15.515008+00:00", + "duration": 0.023944, + "end_time": "2026-09-30T05:47:48.393484+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.508437+00:00", + "start_time": "2026-09-30T05:47:48.369540+00:00", "status": "completed" }, "tags": [] @@ -3507,16 +3555,16 @@ "id": "f32f45f1", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:15.529916Z", - "iopub.status.busy": "2026-06-07T15:28:15.529756Z", - "iopub.status.idle": "2026-06-07T15:28:15.646658Z", - "shell.execute_reply": "2026-06-07T15:28:15.645769Z" + "iopub.execute_input": "2026-09-30T05:47:48.454041Z", + "iopub.status.busy": "2026-09-30T05:47:48.453832Z", + "iopub.status.idle": "2026-09-30T05:47:48.622222Z", + "shell.execute_reply": "2026-09-30T05:47:48.621231Z" }, "papermill": { - "duration": 0.125539, - "end_time": "2026-06-07T15:28:15.647554+00:00", + "duration": 0.20084, + "end_time": "2026-09-30T05:47:48.622900+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.522015+00:00", + "start_time": "2026-09-30T05:47:48.422060+00:00", "status": "completed" }, "tags": [] @@ -3535,7 +3583,7 @@ " \n", "
\n", " 
-- NOTE: `ring` est une tactique Mathlib, pas disponible en Lean 4 standard.
\n", - "
-- Nous verrons `ring` en detail dans Lean-6-Mathlib-Essentials.
\n", + "
-- Nous verrons `ring` en detail dans Lean-06-Mathlib-Essentials-Lean.
\n", "
\n", "
-- Voici ce que `ring` ferait automatiquement :
\n", "
-- theorem ring_example (a b : Int) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring
\n", @@ -3551,7 +3599,7 @@ "
\n", "
\n", " Raw input\n", - " {\"cmd\": \"-- NOTE: `ring` est une tactique Mathlib, pas disponible en Lean 4 standard.\\n-- Nous verrons `ring` en detail dans Lean-6-Mathlib-Essentials.\\n\\n-- Voici ce que `ring` ferait automatiquement :\\n-- theorem ring_example (a b : Int) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring\\n\\n-- Sans Mathlib, on utilise simp et les lemmes arithmetiques standards\\n-- pour des egalites plus simples\\ntheorem double_eq (n : Nat) : n + n = 2 * n := by\\n simp [Nat.two_mul]\\n\\ntheorem simple_arith (a b : Nat) : (a + b) + b = a + 2 * b := by\\n rw [Nat.two_mul, Nat.add_assoc]\", \"env\": 26}\n", + " {\"cmd\": \"-- NOTE: `ring` est une tactique Mathlib, pas disponible en Lean 4 standard.\\n-- Nous verrons `ring` en detail dans Lean-06-Mathlib-Essentials-Lean.\\n\\n-- Voici ce que `ring` ferait automatiquement :\\n-- theorem ring_example (a b : Int) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring\\n\\n-- Sans Mathlib, on utilise simp et les lemmes arithmetiques standards\\n-- pour des egalites plus simples\\ntheorem double_eq (n : Nat) : n + n = 2 * n := by\\n simp [Nat.two_mul]\\n\\ntheorem simple_arith (a b : Nat) : (a + b) + b = a + 2 * b := by\\n rw [Nat.two_mul, Nat.add_assoc]\", \"env\": 26}\n", "
\n", "
\n", " Raw output\n", @@ -3561,7 +3609,7 @@ ], "text/plain": [ "-- NOTE: `ring` est une tactique Mathlib, pas disponible en Lean 4 standard.\n", - "-- Nous verrons `ring` en detail dans Lean-6-Mathlib-Essentials.\n", + "-- Nous verrons `ring` en detail dans Lean-06-Mathlib-Essentials-Lean.\n", "\n", "-- Voici ce que `ring` ferait automatiquement :\n", "-- theorem ring_example (a b : Int) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring\n", @@ -3576,7 +3624,7 @@ "--% env 27\n", "\n", "Raw input:\n", - "{\"cmd\": \"-- NOTE: `ring` est une tactique Mathlib, pas disponible en Lean 4 standard.\\n-- Nous verrons `ring` en detail dans Lean-6-Mathlib-Essentials.\\n\\n-- Voici ce que `ring` ferait automatiquement :\\n-- theorem ring_example (a b : Int) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring\\n\\n-- Sans Mathlib, on utilise simp et les lemmes arithmetiques standards\\n-- pour des egalites plus simples\\ntheorem double_eq (n : Nat) : n + n = 2 * n := by\\n simp [Nat.two_mul]\\n\\ntheorem simple_arith (a b : Nat) : (a + b) + b = a + 2 * b := by\\n rw [Nat.two_mul, Nat.add_assoc]\", \"env\": 26}\n", + "{\"cmd\": \"-- NOTE: `ring` est une tactique Mathlib, pas disponible en Lean 4 standard.\\n-- Nous verrons `ring` en detail dans Lean-06-Mathlib-Essentials-Lean.\\n\\n-- Voici ce que `ring` ferait automatiquement :\\n-- theorem ring_example (a b : Int) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring\\n\\n-- Sans Mathlib, on utilise simp et les lemmes arithmetiques standards\\n-- pour des egalites plus simples\\ntheorem double_eq (n : Nat) : n + n = 2 * n := by\\n simp [Nat.two_mul]\\n\\ntheorem simple_arith (a b : Nat) : (a + b) + b = a + 2 * b := by\\n rw [Nat.two_mul, Nat.add_assoc]\", \"env\": 26}\n", "Raw output:\n", "{\"env\": 27}" ] @@ -3587,7 +3635,7 @@ ], "source": [ "-- NOTE: `ring` est une tactique Mathlib, pas disponible en Lean 4 standard.\n", - "-- Nous verrons `ring` en detail dans Lean-6-Mathlib-Essentials.\n", + "-- Nous verrons `ring` en detail dans Lean-06-Mathlib-Essentials-Lean.\n", "\n", "-- Voici ce que `ring` ferait automatiquement :\n", "-- theorem ring_example (a b : Int) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring\n", @@ -3606,10 +3654,10 @@ "id": "b189bc94", "metadata": { "papermill": { - "duration": 0.006864, - "end_time": "2026-06-07T15:28:15.661234+00:00", + "duration": 0.027884, + "end_time": "2026-09-30T05:47:48.679912+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.654370+00:00", + "start_time": "2026-09-30T05:47:48.652028+00:00", "status": "completed" }, "tags": [] @@ -3644,16 +3692,16 @@ "id": "b4ec3331", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:15.675045Z", - "iopub.status.busy": "2026-06-07T15:28:15.674871Z", - "iopub.status.idle": "2026-06-07T15:28:15.788002Z", - "shell.execute_reply": "2026-06-07T15:28:15.787161Z" + "iopub.execute_input": "2026-09-30T05:47:48.737332Z", + "iopub.status.busy": "2026-09-30T05:47:48.737140Z", + "iopub.status.idle": "2026-09-30T05:47:48.920004Z", + "shell.execute_reply": "2026-09-30T05:47:48.918591Z" }, "papermill": { - "duration": 0.120909, - "end_time": "2026-06-07T15:28:15.788441+00:00", + "duration": 0.209907, + "end_time": "2026-09-30T05:47:48.920611+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.667532+00:00", + "start_time": "2026-09-30T05:47:48.710704+00:00", "status": "completed" }, "tags": [] @@ -3730,6 +3778,13 @@ "cell_type": "markdown", "id": "b7581007", "metadata": { + "papermill": { + "duration": 0.028734, + "end_time": "2026-09-30T05:47:48.984189+00:00", + "exception": false, + "start_time": "2026-09-30T05:47:48.955455+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -3741,10 +3796,10 @@ "id": "c856651d", "metadata": { "papermill": { - "duration": 0.006105, - "end_time": "2026-06-07T15:28:15.801011+00:00", + "duration": 0.026864, + "end_time": "2026-09-30T05:47:49.039157+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.794906+00:00", + "start_time": "2026-09-30T05:47:49.012293+00:00", "status": "completed" }, "tags": [] @@ -3790,16 +3845,16 @@ "id": "37f1d764", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:15.813986Z", - "iopub.status.busy": "2026-06-07T15:28:15.813839Z", - "iopub.status.idle": "2026-06-07T15:28:15.920851Z", - "shell.execute_reply": "2026-06-07T15:28:15.920207Z" + "iopub.execute_input": "2026-09-30T05:47:49.087757Z", + "iopub.status.busy": "2026-09-30T05:47:49.087570Z", + "iopub.status.idle": "2026-09-30T05:47:49.242442Z", + "shell.execute_reply": "2026-09-30T05:47:49.241630Z" }, "papermill": { - "duration": 0.114675, - "end_time": "2026-06-07T15:28:15.921543+00:00", + "duration": 0.17813, + "end_time": "2026-09-30T05:47:49.243802+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.806868+00:00", + "start_time": "2026-09-30T05:47:49.065672+00:00", "status": "completed" }, "tags": [] @@ -3873,6 +3928,13 @@ "cell_type": "markdown", "id": "b7601008", "metadata": { + "papermill": { + "duration": 0.02443, + "end_time": "2026-09-30T05:47:49.292735+00:00", + "exception": false, + "start_time": "2026-09-30T05:47:49.268305+00:00", + "status": "completed" + }, "tags": [] }, "source": [ @@ -3884,10 +3946,10 @@ "id": "4ac1958b", "metadata": { "papermill": { - "duration": 0.00607, - "end_time": "2026-06-07T15:28:15.933956+00:00", + "duration": 0.023661, + "end_time": "2026-09-30T05:47:49.344399+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.927886+00:00", + "start_time": "2026-09-30T05:47:49.320738+00:00", "status": "completed" }, "tags": [] @@ -3908,16 +3970,16 @@ "id": "80ef06cc", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:15.946409Z", - "iopub.status.busy": "2026-06-07T15:28:15.946281Z", - "iopub.status.idle": "2026-06-07T15:28:16.090941Z", - "shell.execute_reply": "2026-06-07T15:28:16.090201Z" + "iopub.execute_input": "2026-09-30T05:47:49.398599Z", + "iopub.status.busy": "2026-09-30T05:47:49.398412Z", + "iopub.status.idle": "2026-09-30T05:47:49.594604Z", + "shell.execute_reply": "2026-09-30T05:47:49.593452Z" }, "papermill": { - "duration": 0.152561, - "end_time": "2026-06-07T15:28:16.092191+00:00", + "duration": 0.224452, + "end_time": "2026-09-30T05:47:49.595489+00:00", "exception": false, - "start_time": "2026-06-07T15:28:15.939630+00:00", + "start_time": "2026-09-30T05:47:49.371037+00:00", "status": "completed" }, "tags": [] @@ -4166,10 +4228,10 @@ "id": "d532845b", "metadata": { "papermill": { - "duration": 0.007247, - "end_time": "2026-06-07T15:28:16.107497+00:00", + "duration": 0.037048, + "end_time": "2026-09-30T05:47:49.657459+00:00", "exception": false, - "start_time": "2026-06-07T15:28:16.100250+00:00", + "start_time": "2026-09-30T05:47:49.620411+00:00", "status": "completed" }, "tags": [] @@ -4190,17 +4252,17 @@ "id": "0b2e60f0", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:16.123881Z", - "iopub.status.busy": "2026-06-07T15:28:16.123732Z", - "iopub.status.idle": "2026-06-07T15:28:16.231648Z", - "shell.execute_reply": "2026-06-07T15:28:16.230287Z" + "iopub.execute_input": "2026-09-30T05:47:49.721793Z", + "iopub.status.busy": "2026-09-30T05:47:49.721558Z", + "iopub.status.idle": "2026-09-30T05:47:49.891241Z", + "shell.execute_reply": "2026-09-30T05:47:49.889976Z" }, "language": "lean4", "papermill": { - "duration": 0.117093, - "end_time": "2026-06-07T15:28:16.232516+00:00", + "duration": 0.202457, + "end_time": "2026-09-30T05:47:49.892142+00:00", "exception": false, - "start_time": "2026-06-07T15:28:16.115423+00:00", + "start_time": "2026-09-30T05:47:49.689685+00:00", "status": "completed" }, "tags": [] @@ -4285,10 +4347,10 @@ "id": "0cc13061", "metadata": { "papermill": { - "duration": 0.007512, - "end_time": "2026-06-07T15:28:16.247773+00:00", + "duration": 0.024063, + "end_time": "2026-09-30T05:47:49.942460+00:00", "exception": false, - "start_time": "2026-06-07T15:28:16.240261+00:00", + "start_time": "2026-09-30T05:47:49.918397+00:00", "status": "completed" }, "tags": [] @@ -4305,17 +4367,17 @@ "id": "1dcfda73", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:16.264970Z", - "iopub.status.busy": "2026-06-07T15:28:16.264797Z", - "iopub.status.idle": "2026-06-07T15:28:16.372730Z", - "shell.execute_reply": "2026-06-07T15:28:16.371822Z" + "iopub.execute_input": "2026-09-30T05:47:50.014636Z", + "iopub.status.busy": "2026-09-30T05:47:50.014438Z", + "iopub.status.idle": "2026-09-30T05:47:50.168217Z", + "shell.execute_reply": "2026-09-30T05:47:50.167261Z" }, "language": "lean4", "papermill": { - "duration": 0.117475, - "end_time": "2026-06-07T15:28:16.373334+00:00", + "duration": 0.19907, + "end_time": "2026-09-30T05:47:50.168807+00:00", "exception": false, - "start_time": "2026-06-07T15:28:16.255859+00:00", + "start_time": "2026-09-30T05:47:49.969737+00:00", "status": "completed" }, "tags": [] @@ -4403,10 +4465,10 @@ "id": "5bb9f488", "metadata": { "papermill": { - "duration": 0.007451, - "end_time": "2026-06-07T15:28:16.388473+00:00", + "duration": 0.025915, + "end_time": "2026-09-30T05:47:50.225383+00:00", "exception": false, - "start_time": "2026-06-07T15:28:16.381022+00:00", + "start_time": "2026-09-30T05:47:50.199468+00:00", "status": "completed" }, "tags": [] @@ -4423,17 +4485,17 @@ "id": "5d40d3cf", "metadata": { "execution": { - "iopub.execute_input": "2026-06-07T15:28:16.402897Z", - "iopub.status.busy": "2026-06-07T15:28:16.402747Z", - "iopub.status.idle": "2026-06-07T15:28:16.509749Z", - "shell.execute_reply": "2026-06-07T15:28:16.508926Z" + "iopub.execute_input": "2026-09-30T05:47:50.276885Z", + "iopub.status.busy": "2026-09-30T05:47:50.276707Z", + "iopub.status.idle": "2026-09-30T05:47:50.430422Z", + "shell.execute_reply": "2026-09-30T05:47:50.429061Z" }, "language": "lean4", "papermill": { - "duration": 0.115122, - "end_time": "2026-06-07T15:28:16.510425+00:00", + "duration": 0.180777, + "end_time": "2026-09-30T05:47:50.431138+00:00", "exception": false, - "start_time": "2026-06-07T15:28:16.395303+00:00", + "start_time": "2026-09-30T05:47:50.250361+00:00", "status": "completed" }, "tags": [] @@ -4518,10 +4580,10 @@ "id": "9bd5a610", "metadata": { "papermill": { - "duration": 0.007943, - "end_time": "2026-06-07T15:28:16.526162+00:00", + "duration": 0.024818, + "end_time": "2026-09-30T05:47:50.480088+00:00", "exception": false, - "start_time": "2026-06-07T15:28:16.518219+00:00", + "start_time": "2026-09-30T05:47:50.455270+00:00", "status": "completed" }, "tags": [] @@ -4562,7 +4624,17 @@ }, { "cell_type": "markdown", - "metadata": {}, + "id": "1ce5bd73", + "metadata": { + "papermill": { + "duration": 0.024918, + "end_time": "2026-09-30T05:47:50.529766+00:00", + "exception": false, + "start_time": "2026-09-30T05:47:50.504848+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "## Lire une preuve : classifier par tactique d'ouverture\n", "\n", @@ -4603,21 +4675,21 @@ "name": "lean4" }, "language_info": { - "codemirror_mode": "python", + "codemirror_mode": "lean4", "file_extension": ".lean", "mimetype": "text/x-lean4", "name": "lean4" }, "papermill": { "default_parameters": {}, - "duration": 9.434021, - "end_time": "2026-06-07T15:28:16.748113+00:00", + "duration": 129.485062, + "end_time": "2026-09-30T05:47:50.766988+00:00", "environment_variables": {}, "exception": null, "input_path": "Lean-05-Tactics-Lean.ipynb", "output_path": "Lean-05-Tactics-Lean.ipynb", "parameters": {}, - "start_time": "2026-06-07T15:28:07.314092+00:00", + "start_time": "2026-09-30T05:45:41.281926+00:00", "version": "2.7.0" } },