diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb index e6aff97c71..34302c78df 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb @@ -5,10 +5,10 @@ "id": "6b836eaa", "metadata": { "papermill": { - "duration": 0.007864, - "end_time": "2026-06-09T00:36:48.765593+00:00", + "duration": 0.009299, + "end_time": "2026-09-24T11:38:47.694262+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.757729+00:00", + "start_time": "2026-09-24T11:38:47.684963+00:00", "status": "completed" }, "tags": [] @@ -79,10 +79,10 @@ "id": "b698abc9", "metadata": { "papermill": { - "duration": 0.004453, - "end_time": "2026-06-09T00:36:48.781245+00:00", + "duration": 0.004641, + "end_time": "2026-09-24T11:38:47.704411+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.776792+00:00", + "start_time": "2026-09-24T11:38:47.699770+00:00", "status": "completed" }, "tags": [] @@ -124,10 +124,10 @@ "id": "e7be3e9d", "metadata": { "papermill": { - "duration": 0.003454, - "end_time": "2026-06-09T00:36:48.788036+00:00", + "duration": 0.004767, + "end_time": "2026-09-24T11:38:47.713785+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.784582+00:00", + "start_time": "2026-09-24T11:38:47.709018+00:00", "status": "completed" }, "tags": [] @@ -147,10 +147,10 @@ "id": "42772afa", "metadata": { "papermill": { - "duration": 0.004731, - "end_time": "2026-06-09T00:36:48.796346+00:00", + "duration": 0.004485, + "end_time": "2026-09-24T11:38:47.722969+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.791615+00:00", + "start_time": "2026-09-24T11:38:47.718484+00:00", "status": "completed" }, "tags": [] @@ -185,10 +185,10 @@ "id": "9dfb3c5c", "metadata": { "papermill": { - "duration": 0.004556, - "end_time": "2026-06-09T00:36:48.805021+00:00", + "duration": 0.004888, + "end_time": "2026-09-24T11:38:47.732427+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.800465+00:00", + "start_time": "2026-09-24T11:38:47.727539+00:00", "status": "completed" }, "tags": [] @@ -235,10 +235,10 @@ "id": "21bb5fe1", "metadata": { "papermill": { - "duration": 0.003684, - "end_time": "2026-06-09T00:36:48.812403+00:00", + "duration": 0.004464, + "end_time": "2026-09-24T11:38:47.742088+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.808719+00:00", + "start_time": "2026-09-24T11:38:47.737624+00:00", "status": "completed" }, "tags": [] @@ -269,10 +269,10 @@ "id": "7ad5638e", "metadata": { "papermill": { - "duration": 0.003837, - "end_time": "2026-06-09T00:36:48.819962+00:00", + "duration": 0.00495, + "end_time": "2026-09-24T11:38:47.751453+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.816125+00:00", + "start_time": "2026-09-24T11:38:47.746503+00:00", "status": "completed" }, "tags": [] @@ -310,10 +310,10 @@ "id": "d11ec519", "metadata": { "papermill": { - "duration": 0.004056, - "end_time": "2026-06-09T00:36:48.827994+00:00", + "duration": 0.004579, + "end_time": "2026-09-24T11:38:47.760474+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.823938+00:00", + "start_time": "2026-09-24T11:38:47.755895+00:00", "status": "completed" }, "tags": [] @@ -378,10 +378,10 @@ "id": "eaa51d87", "metadata": { "papermill": { - "duration": 0.003793, - "end_time": "2026-06-09T00:36:48.835690+00:00", + "duration": 0.004371, + "end_time": "2026-09-24T11:38:47.770267+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.831897+00:00", + "start_time": "2026-09-24T11:38:47.765896+00:00", "status": "completed" }, "tags": [] @@ -405,10 +405,10 @@ "id": "8fec9966", "metadata": { "papermill": { - "duration": 0.003852, - "end_time": "2026-06-09T00:36:48.843328+00:00", + "duration": 0.004251, + "end_time": "2026-09-24T11:38:47.778840+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.839476+00:00", + "start_time": "2026-09-24T11:38:47.774589+00:00", "status": "completed" }, "tags": [] @@ -432,10 +432,10 @@ "id": "00339661", "metadata": { "papermill": { - "duration": 0.003856, - "end_time": "2026-06-09T00:36:48.850886+00:00", + "duration": 0.004518, + "end_time": "2026-09-24T11:38:47.787989+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.847030+00:00", + "start_time": "2026-09-24T11:38:47.783471+00:00", "status": "completed" }, "tags": [] @@ -458,10 +458,10 @@ "id": "3d877df4", "metadata": { "papermill": { - "duration": 0.003602, - "end_time": "2026-06-09T00:36:48.858193+00:00", + "duration": 0.006371, + "end_time": "2026-09-24T11:38:47.798820+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.854591+00:00", + "start_time": "2026-09-24T11:38:47.792449+00:00", "status": "completed" }, "tags": [] @@ -507,10 +507,10 @@ "id": "a3c1e054", "metadata": { "papermill": { - "duration": 0.00381, - "end_time": "2026-06-09T00:36:48.865715+00:00", + "duration": 0.004514, + "end_time": "2026-09-24T11:38:47.808144+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.861905+00:00", + "start_time": "2026-09-24T11:38:47.803630+00:00", "status": "completed" }, "tags": [] @@ -532,10 +532,10 @@ "id": "c2093ba7", "metadata": { "papermill": { - "duration": 0.003596, - "end_time": "2026-06-09T00:36:48.875391+00:00", + "duration": 0.004776, + "end_time": "2026-09-24T11:38:47.817683+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.871795+00:00", + "start_time": "2026-09-24T11:38:47.812907+00:00", "status": "completed" }, "tags": [] @@ -561,10 +561,10 @@ "id": "3c2008ea", "metadata": { "papermill": { - "duration": 0.003617, - "end_time": "2026-06-09T00:36:48.882784+00:00", + "duration": 0.004743, + "end_time": "2026-09-24T11:38:47.827008+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.879167+00:00", + "start_time": "2026-09-24T11:38:47.822265+00:00", "status": "completed" }, "tags": [] @@ -587,7 +587,7 @@ "| MathlibMap | `Conway/MathlibMap.lean` | 10 `#check` Conway-adjacents dans Mathlib |\n", "\n", "Le depot heberge aussi un **second projet Lake indépendant**, `conway_cgt_lean/`\n", - "(toolchain `v4.31.0-rc1`), qui importe [`vihdzp/combinatorial-games`](https://github.com/vihdzp/combinatorial-games)\n", + "(toolchain `v4.31.0-rc2`), qui importe [`vihdzp/combinatorial-games`](https://github.com/vihdzp/combinatorial-games)\n", "et presente les résultats centraux de Conway en théorie des jeux :\n", "\n", "| Thème | Fichier | Contenu |\n", @@ -605,17 +605,17 @@ "id": "25c66a78", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T00:36:48.891385Z", - "iopub.status.busy": "2026-06-09T00:36:48.891187Z", - "iopub.status.idle": "2026-06-09T00:36:48.905878Z", - "shell.execute_reply": "2026-06-09T00:36:48.905287Z" + "iopub.execute_input": "2026-09-24T11:38:47.837957Z", + "iopub.status.busy": "2026-09-24T11:38:47.837664Z", + "iopub.status.idle": "2026-09-24T11:38:47.851987Z", + "shell.execute_reply": "2026-09-24T11:38:47.851180Z" }, "id": "subprocess-setup", "papermill": { - "duration": 0.020158, - "end_time": "2026-06-09T00:36:48.906679+00:00", + "duration": 0.021093, + "end_time": "2026-09-24T11:38:47.852929+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.886521+00:00", + "start_time": "2026-09-24T11:38:47.831836+00:00", "status": "completed" }, "tags": [] @@ -672,17 +672,17 @@ "id": "ffe03c0f", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T00:36:48.915226Z", - "iopub.status.busy": "2026-06-09T00:36:48.915036Z", - "iopub.status.idle": "2026-06-09T00:36:48.920910Z", - "shell.execute_reply": "2026-06-09T00:36:48.920086Z" + "iopub.execute_input": "2026-09-24T11:38:47.864926Z", + "iopub.status.busy": "2026-09-24T11:38:47.864596Z", + "iopub.status.idle": "2026-09-24T11:38:47.871247Z", + "shell.execute_reply": "2026-09-24T11:38:47.870295Z" }, "id": "lean-readers", "papermill": { - "duration": 0.011927, - "end_time": "2026-06-09T00:36:48.922233+00:00", + "duration": 0.014363, + "end_time": "2026-09-24T11:38:47.871959+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.910306+00:00", + "start_time": "2026-09-24T11:38:47.857596+00:00", "status": "completed" }, "tags": [] @@ -733,10 +733,10 @@ "id": "d249943a", "metadata": { "papermill": { - "duration": 0.003563, - "end_time": "2026-06-09T00:36:48.929484+00:00", + "duration": 0.004548, + "end_time": "2026-09-24T11:38:47.881398+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.925921+00:00", + "start_time": "2026-09-24T11:38:47.876850+00:00", "status": "completed" }, "tags": [] @@ -754,17 +754,17 @@ "id": "8a921651", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T00:36:48.938029Z", - "iopub.status.busy": "2026-06-09T00:36:48.937827Z", - "iopub.status.idle": "2026-06-09T00:36:48.943513Z", - "shell.execute_reply": "2026-06-09T00:36:48.942885Z" + "iopub.execute_input": "2026-09-24T11:38:47.892709Z", + "iopub.status.busy": "2026-09-24T11:38:47.892344Z", + "iopub.status.idle": "2026-09-24T11:38:47.901325Z", + "shell.execute_reply": "2026-09-24T11:38:47.900480Z" }, "id": "doomsday-decls", "papermill": { - "duration": 0.011153, - "end_time": "2026-06-09T00:36:48.944191+00:00", + "duration": 0.016172, + "end_time": "2026-09-24T11:38:47.902116+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.933038+00:00", + "start_time": "2026-09-24T11:38:47.885944+00:00", "status": "completed" }, "tags": [] @@ -774,12 +774,12 @@ "name": "stdout", "output_type": "stream", "text": [ - "=== Conway/DoomsdayLemmas.lean (46 lignes, sorry reels = 0) ===\n", - " L 25 theorem isLeapYear_2000\n", - " L 29 theorem isLeapYear_1900\n", - " L 33 theorem isLeapYear_2024\n", - " L 38 theorem dayOfWeek_conway_death\n", - " L 43 theorem dayOfWeek_add_seven\n" + "=== Conway/DoomsdayLemmas.lean (52 lignes, sorry reels = 0) ===\n", + " L 31 theorem isLeapYear_2000\n", + " L 35 theorem isLeapYear_1900\n", + " L 39 theorem isLeapYear_2024\n", + " L 44 theorem dayOfWeek_conway_death\n", + " L 49 theorem dayOfWeek_add_seven\n" ] }, { @@ -802,10 +802,10 @@ "id": "6548c2b6", "metadata": { "papermill": { - "duration": 0.004038, - "end_time": "2026-06-09T00:36:48.952133+00:00", + "duration": 0.004817, + "end_time": "2026-09-24T11:38:47.912459+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.948095+00:00", + "start_time": "2026-09-24T11:38:47.907642+00:00", "status": "completed" }, "tags": [] @@ -823,17 +823,17 @@ "id": "c2528f8e", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T00:36:48.961959Z", - "iopub.status.busy": "2026-06-09T00:36:48.961755Z", - "iopub.status.idle": "2026-06-09T00:36:48.966309Z", - "shell.execute_reply": "2026-06-09T00:36:48.965705Z" + "iopub.execute_input": "2026-09-24T11:38:47.923229Z", + "iopub.status.busy": "2026-09-24T11:38:47.922946Z", + "iopub.status.idle": "2026-09-24T11:38:47.929879Z", + "shell.execute_reply": "2026-09-24T11:38:47.929072Z" }, "id": "looksay-decls", "papermill": { - "duration": 0.010632, - "end_time": "2026-06-09T00:36:48.966976+00:00", + "duration": 0.013392, + "end_time": "2026-09-24T11:38:47.930487+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.956344+00:00", + "start_time": "2026-09-24T11:38:47.917095+00:00", "status": "completed" }, "tags": [] @@ -843,10 +843,10 @@ "name": "stdout", "output_type": "stream", "text": [ - "=== Conway/LookAndSayLemmas.lean (55 lignes, sorry reels = 0) ===\n", - " L 25 theorem digitsToNat_example\n", - " L 29 theorem lookAndSay_4\n", - " L 34 theorem digitsToNat_natToDigits\n" + "=== Conway/LookAndSayLemmas.lean (62 lignes, sorry reels = 0) ===\n", + " L 32 theorem digitsToNat_example\n", + " L 36 theorem lookAndSay_4\n", + " L 41 theorem digitsToNat_natToDigits\n" ] }, { @@ -869,10 +869,10 @@ "id": "6a917c75", "metadata": { "papermill": { - "duration": 0.004014, - "end_time": "2026-06-09T00:36:48.974919+00:00", + "duration": 0.004974, + "end_time": "2026-09-24T11:38:47.940361+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.970905+00:00", + "start_time": "2026-09-24T11:38:47.935387+00:00", "status": "completed" }, "tags": [] @@ -891,17 +891,17 @@ "id": "51a2ac19", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T00:36:48.984812Z", - "iopub.status.busy": "2026-06-09T00:36:48.984596Z", - "iopub.status.idle": "2026-06-09T00:36:48.989399Z", - "shell.execute_reply": "2026-06-09T00:36:48.988696Z" + "iopub.execute_input": "2026-09-24T11:38:47.951848Z", + "iopub.status.busy": "2026-09-24T11:38:47.951495Z", + "iopub.status.idle": "2026-09-24T11:38:47.959266Z", + "shell.execute_reply": "2026-09-24T11:38:47.958273Z" }, "id": "nim-decls", "papermill": { - "duration": 0.010893, - "end_time": "2026-06-09T00:36:48.990088+00:00", + "duration": 0.014596, + "end_time": "2026-09-24T11:38:47.960129+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.979195+00:00", + "start_time": "2026-09-24T11:38:47.945533+00:00", "status": "completed" }, "tags": [] @@ -911,24 +911,24 @@ "name": "stdout", "output_type": "stream", "text": [ - "=== Conway/Nim.lean (138 lignes, sorry reels = 0) ===\n", - " L 25 def nimSum\n", - " L 29 def isWinningNim\n", - " L 38 theorem nimSum_nil\n", - " L 41 theorem isWinningNim_345\n", - " L 45 theorem nimSum_single\n", - " L 49 theorem nimSum_self\n", - " L 69 theorem isWinningNim_357\n", - " L 80 theorem nimStrategy_357\n", - " L 85 theorem xor_zero\n", - " L 89 theorem xor_comm\n", - " L 93 theorem xor_assoc\n", - " L 97 theorem nimSum3_assoc\n", - " L 103 theorem winning_move_357\n", - " L 111 theorem losing_position_123\n", - " L 116 theorem all_moves_from_123_winning\n", - " L 127 theorem xor_reduce_3_1\n", - " L 131 theorem winning_move_verified_357\n" + "=== Conway/Nim.lean (156 lignes, sorry reels = 0) ===\n", + " L 41 def nimSum\n", + " L 45 def isWinningNim\n", + " L 54 theorem nimSum_nil\n", + " L 57 theorem isWinningNim_345\n", + " L 61 theorem nimSum_single\n", + " L 65 theorem nimSum_self\n", + " L 86 theorem isWinningNim_357\n", + " L 97 theorem nimStrategy_357\n", + " L 102 theorem xor_zero\n", + " L 106 theorem xor_comm\n", + " L 110 theorem xor_assoc\n", + " L 114 theorem nimSum3_assoc\n", + " L 120 theorem winning_move_357\n", + " L 128 theorem losing_position_123\n", + " L 133 theorem all_moves_from_123_winning\n", + " L 144 theorem xor_reduce_3_1\n", + " L 148 theorem winning_move_verified_357\n" ] }, { @@ -951,10 +951,10 @@ "id": "fd966474", "metadata": { "papermill": { - "duration": 0.003788, - "end_time": "2026-06-09T00:36:48.998195+00:00", + "duration": 0.005301, + "end_time": "2026-09-24T11:38:47.970405+00:00", "exception": false, - "start_time": "2026-06-09T00:36:48.994407+00:00", + "start_time": "2026-09-24T11:38:47.965104+00:00", "status": "completed" }, "tags": [] @@ -973,17 +973,17 @@ "id": "ca8e8772", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T00:36:49.007721Z", - "iopub.status.busy": "2026-06-09T00:36:49.007530Z", - "iopub.status.idle": "2026-06-09T00:36:49.012133Z", - "shell.execute_reply": "2026-06-09T00:36:49.011582Z" + "iopub.execute_input": "2026-09-24T11:38:47.981336Z", + "iopub.status.busy": "2026-09-24T11:38:47.981005Z", + "iopub.status.idle": "2026-09-24T11:38:47.986040Z", + "shell.execute_reply": "2026-09-24T11:38:47.985284Z" }, "id": "angel-decls", "papermill": { - "duration": 0.010397, - "end_time": "2026-06-09T00:36:49.012676+00:00", + "duration": 0.011314, + "end_time": "2026-09-24T11:38:47.986633+00:00", "exception": false, - "start_time": "2026-06-09T00:36:49.002279+00:00", + "start_time": "2026-09-24T11:38:47.975319+00:00", "status": "completed" }, "tags": [] @@ -993,13 +993,13 @@ "name": "stdout", "output_type": "stream", "text": [ - "=== Conway/Angel.lean (65 lignes, sorry reels = 0) ===\n", - " L 29 def chebyshev\n", - " L 34 def angelMoves\n", - " L 43 theorem chebyshev_self\n", - " L 47 theorem kingMoves_card\n", - " L 51 theorem angelMoves2_card\n", - " L 57 theorem angelMoves_card\n" + "=== Conway/Angel.lean (77 lignes, sorry reels = 0) ===\n", + " L 41 def chebyshev\n", + " L 46 def angelMoves\n", + " L 55 theorem chebyshev_self\n", + " L 59 theorem kingMoves_card\n", + " L 63 theorem angelMoves2_card\n", + " L 69 theorem angelMoves_card\n" ] }, { @@ -1022,10 +1022,10 @@ "id": "1be7b8c0", "metadata": { "papermill": { - "duration": 0.003676, - "end_time": "2026-06-09T00:36:49.020205+00:00", + "duration": 0.004549, + "end_time": "2026-09-24T11:38:47.995879+00:00", "exception": false, - "start_time": "2026-06-09T00:36:49.016529+00:00", + "start_time": "2026-09-24T11:38:47.991330+00:00", "status": "completed" }, "tags": [] @@ -1045,17 +1045,17 @@ "id": "75608618", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T00:36:49.028963Z", - "iopub.status.busy": "2026-06-09T00:36:49.028664Z", - "iopub.status.idle": "2026-06-09T00:36:49.033467Z", - "shell.execute_reply": "2026-06-09T00:36:49.032870Z" + "iopub.execute_input": "2026-09-24T11:38:48.006411Z", + "iopub.status.busy": "2026-09-24T11:38:48.006211Z", + "iopub.status.idle": "2026-09-24T11:38:48.012318Z", + "shell.execute_reply": "2026-09-24T11:38:48.011661Z" }, "id": "life-decls", "papermill": { - "duration": 0.010115, - "end_time": "2026-06-09T00:36:49.034093+00:00", + "duration": 0.012196, + "end_time": "2026-09-24T11:38:48.012856+00:00", "exception": false, - "start_time": "2026-06-09T00:36:49.023978+00:00", + "start_time": "2026-09-24T11:38:48.000660+00:00", "status": "completed" }, "tags": [] @@ -1065,35 +1065,37 @@ "name": "stdout", "output_type": "stream", "text": [ - "=== Conway/Life.lean (202 lignes, sorry reels = 0) ===\n", - " L 47 def lexLt\n", - " L 55 abbrev Grid\n", - " L 64 def mooreNeighbors\n", - " L 78 def isAlive\n", - " L 82 def liveNeighborCount\n", - " L 86 def aliveNext\n", - " L 94 def candidates\n", - " L 98 def sortDedup\n", - " L 102 def step\n", - " L 106 def evolve\n", - " L 123 def isStillLife\n", - " L 126 def isOscillator\n", - " L 129 def shift\n", - " L 134 def isSpaceship\n", - " L 149 def block\n", - " L 152 def beehive\n", - " L 155 def blinker_h\n", - " L 158 def blinker_v\n", - " L 161 def toad\n", - " L 164 def beacon\n", - " L 169 def glider\n", - " L 181 theorem block_still_life\n", - " L 184 theorem beehive_still_life\n", - " L 187 theorem blinker_period_two\n", - " L 190 theorem blinker_step\n", - " L 193 theorem toad_period_two\n", - " L 196 theorem beacon_period_two\n", - " L 199 theorem glider_spaceship\n" + "=== Conway/Life.lean (253 lignes, sorry reels = 0) ===\n", + " L 57 def lexLt\n", + " L 67 abbrev Grid\n", + " L 77 def mooreNeighbors\n", + " L 91 def isAlive\n", + " L 95 def liveNeighborCount\n", + " L 99 def aliveNext\n", + " L 107 def candidates\n", + " L 115 def lexLe\n", + " L 138 def sortDedup\n", + " L 146 theorem mem_sortDedup\n", + " L 152 def step\n", + " L 156 def evolve\n", + " L 174 def isStillLife\n", + " L 177 def isOscillator\n", + " L 180 def shift\n", + " L 185 def isSpaceship\n", + " L 200 def block\n", + " L 203 def beehive\n", + " L 206 def blinker_h\n", + " L 209 def blinker_v\n", + " L 212 def toad\n", + " L 215 def beacon\n", + " L 220 def glider\n", + " L 232 theorem block_still_life\n", + " L 235 theorem beehive_still_life\n", + " L 238 theorem blinker_period_two\n", + " L 241 theorem blinker_step\n", + " L 244 theorem toad_period_two\n", + " L 247 theorem beacon_period_two\n", + " L 250 theorem glider_spaceship\n" ] }, { @@ -1116,10 +1118,10 @@ "id": "17e6d8cd", "metadata": { "papermill": { - "duration": 0.004524, - "end_time": "2026-06-09T00:36:49.042582+00:00", + "duration": 0.004061, + "end_time": "2026-09-24T11:38:48.021341+00:00", "exception": false, - "start_time": "2026-06-09T00:36:49.038058+00:00", + "start_time": "2026-09-24T11:38:48.017280+00:00", "status": "completed" }, "tags": [] @@ -1129,7 +1131,7 @@ "\n", "La preuve ultime que ces résultats tiennent : **le module `Conway` compile sans erreur ni sorry**.\n", "On lance `lake build Conway` via WSL (timeout genereux ; a froid le build Mathlib peut etre long,\n", - "auquel cas la vérification CI/PR fait foi). Toolchain : `leanprover/lean4:v4.30.0-rc2`." + "auquel cas la vérification CI/PR fait foi). Toolchain : `leanprover/lean4:v4.32.1`." ] }, { @@ -1138,17 +1140,17 @@ "id": "1972463a", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T00:36:49.053365Z", - "iopub.status.busy": "2026-06-09T00:36:49.053131Z", - "iopub.status.idle": "2026-06-09T01:01:49.075019Z", - "shell.execute_reply": "2026-06-09T01:01:49.072926Z" + "iopub.execute_input": "2026-09-24T11:38:48.031540Z", + "iopub.status.busy": "2026-09-24T11:38:48.031088Z", + "iopub.status.idle": "2026-09-24T11:41:27.730012Z", + "shell.execute_reply": "2026-09-24T11:41:27.728768Z" }, "id": "lake-build", "papermill": { - "duration": 1500.039609, - "end_time": "2026-06-09T01:01:49.086832+00:00", + "duration": 159.709625, + "end_time": "2026-09-24T11:41:27.735211+00:00", "exception": false, - "start_time": "2026-06-09T00:36:49.047223+00:00", + "start_time": "2026-09-24T11:38:48.025586+00:00", "status": "completed" }, "tags": [] @@ -1166,10 +1168,30 @@ "name": "stdout", "output_type": "stream", "text": [ + " simp only [← hn̵e̵_̵l̵v̵l̵,̵ ̵←̵ ̵h̵sw_lvl, ← hse_lvl] at hb\n", "\n", + "Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.\n", "\n", - "Exit code : -1\n", - "TIMEOUT : build a froid trop long ici ; la verification CI/PR est autoritative.\n" + "Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`\n", + "warning: Conway/Life/JumpCapture.lean:511:28: This simp argument is unused:\n", + " ← hsw_lvl\n", + "\n", + "Hint: Omit it from the simp argument list.\n", + " simp only [← hne_lvl, ← hsw̵_̵l̵v̵l̵,̵ ̵←̵ ̵h̵s̵e_lvl] at hb\n", + "\n", + "Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.\n", + "\n", + "Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`\n", + "warning: Conway/Life/JumpCapture.lean:534:36: Variable name `hT` is not explicitly referenced.\n", + "\n", + "The binding can be removed (if unused) or named `_` (if used implicitly).\n", + "\n", + "Note: This linter can be disabled with `set_option linter.unusedVariables false`\n", + "Build completed successfully (8733 jobs).\n", + "\n", + "\n", + "Exit code : 0\n", + "SUCCESS : le module Conway compile (preuves valides, 0 sorry).\n" ] } ], @@ -1199,10 +1221,10 @@ "id": "7852a497", "metadata": { "papermill": { - "duration": 0.011368, - "end_time": "2026-06-09T01:01:49.110640+00:00", + "duration": 0.005427, + "end_time": "2026-09-24T11:41:27.747192+00:00", "exception": false, - "start_time": "2026-06-09T01:01:49.099272+00:00", + "start_time": "2026-09-24T11:41:27.741765+00:00", "status": "completed" }, "tags": [] @@ -1218,17 +1240,17 @@ "id": "cd42a26b", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T01:01:49.137835Z", - "iopub.status.busy": "2026-06-09T01:01:49.137123Z", - "iopub.status.idle": "2026-06-09T01:01:49.151170Z", - "shell.execute_reply": "2026-06-09T01:01:49.149269Z" + "iopub.execute_input": "2026-09-24T11:41:27.761817Z", + "iopub.status.busy": "2026-09-24T11:41:27.761437Z", + "iopub.status.idle": "2026-09-24T11:41:27.769156Z", + "shell.execute_reply": "2026-09-24T11:41:27.768207Z" }, "id": "sorry-scan", "papermill": { - "duration": 0.03031, - "end_time": "2026-06-09T01:01:49.152600+00:00", + "duration": 0.015282, + "end_time": "2026-09-24T11:41:27.769967+00:00", "exception": false, - "start_time": "2026-06-09T01:01:49.122290+00:00", + "start_time": "2026-09-24T11:41:27.754685+00:00", "status": "completed" }, "tags": [] @@ -1271,10 +1293,10 @@ "id": "c26c0bf9", "metadata": { "papermill": { - "duration": 0.010779, - "end_time": "2026-06-09T01:01:49.173954+00:00", + "duration": 0.005142, + "end_time": "2026-09-24T11:41:27.780378+00:00", "exception": false, - "start_time": "2026-06-09T01:01:49.163175+00:00", + "start_time": "2026-09-24T11:41:27.775236+00:00", "status": "completed" }, "tags": [] @@ -1293,17 +1315,17 @@ "id": "6429e8eb", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T01:01:49.197362Z", - "iopub.status.busy": "2026-06-09T01:01:49.196773Z", - "iopub.status.idle": "2026-06-09T01:04:34.724409Z", - "shell.execute_reply": "2026-06-09T01:04:34.722549Z" + "iopub.execute_input": "2026-09-24T11:41:27.792467Z", + "iopub.status.busy": "2026-09-24T11:41:27.792234Z", + "iopub.status.idle": "2026-09-24T11:44:13.508024Z", + "shell.execute_reply": "2026-09-24T11:44:13.507121Z" }, "id": "live-eval", "papermill": { - "duration": 165.550055, - "end_time": "2026-06-09T01:04:34.733935+00:00", + "duration": 165.727283, + "end_time": "2026-09-24T11:44:13.513238+00:00", "exception": false, - "start_time": "2026-06-09T01:01:49.183880+00:00", + "start_time": "2026-09-24T11:41:27.785955+00:00", "status": "completed" }, "tags": [] @@ -1313,9 +1335,13 @@ "name": "stdout", "output_type": "stream", "text": [ - "(pas de sortie)\n", + "\"nimSum [3,4,5] = 2\"\n", + "\"isWinningNim [3,4,5] = true\"\n", + "\"isWinningNim [1,1] = false\"\n", + "\"angelMoves card k=1 (roi) = 8\"\n", + "\"angelMoves card k=2 = 24\"\n", "\n", - "TIMEOUT (>600s) : chargement des oleans trop lent sur ce FS ; la cellule `lake build Conway` ci-dessus reste la preuve que les 5 .lean compilent.\n" + "SUCCESS : calculs Lean exécutés en direct (les définitions réelles tournent).\n" ] } ], @@ -1357,10 +1383,10 @@ "id": "d23b434e", "metadata": { "papermill": { - "duration": 0.009472, - "end_time": "2026-06-09T01:04:34.754831+00:00", + "duration": 0.005999, + "end_time": "2026-09-24T11:44:13.524751+00:00", "exception": false, - "start_time": "2026-06-09T01:04:34.745359+00:00", + "start_time": "2026-09-24T11:44:13.518752+00:00", "status": "completed" }, "tags": [] @@ -1395,16 +1421,16 @@ "id": "f450f5a9", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T01:04:34.780696Z", - "iopub.status.busy": "2026-06-09T01:04:34.780246Z", - "iopub.status.idle": "2026-06-09T01:04:34.792548Z", - "shell.execute_reply": "2026-06-09T01:04:34.791056Z" + "iopub.execute_input": "2026-09-24T11:44:13.537063Z", + "iopub.status.busy": "2026-09-24T11:44:13.536829Z", + "iopub.status.idle": "2026-09-24T11:44:13.543940Z", + "shell.execute_reply": "2026-09-24T11:44:13.542838Z" }, "papermill": { - "duration": 0.026812, - "end_time": "2026-06-09T01:04:34.793755+00:00", + "duration": 0.014746, + "end_time": "2026-09-24T11:44:13.544812+00:00", "exception": false, - "start_time": "2026-06-09T01:04:34.766943+00:00", + "start_time": "2026-09-24T11:44:13.530066+00:00", "status": "completed" }, "tags": [] @@ -1416,7 +1442,7 @@ "text": [ "=== Conway/MathlibMap.lean ===\n", "\n", - " 119 lignes, sorry reels = 0\n", + " 120 lignes, sorry reels = 0\n", " 10 declarations #check (Mathlib showcase)\n", " 0 declarations theorem/def\n", "\n", @@ -1466,10 +1492,10 @@ "id": "fb21226a", "metadata": { "papermill": { - "duration": 0.010137, - "end_time": "2026-06-09T01:04:34.814568+00:00", + "duration": 0.004815, + "end_time": "2026-09-24T11:44:13.554753+00:00", "exception": false, - "start_time": "2026-06-09T01:04:34.804431+00:00", + "start_time": "2026-09-24T11:44:13.549938+00:00", "status": "completed" }, "tags": [] @@ -1484,8 +1510,8 @@ "\n", "Suivant le **pattern Peters** (cf. `social_choice_lean_peters/`), nous importons ce depot comme\n", "dépendance Lake sans dupliquer son code, et nous presentons ses résultats cles via le module\n", - "`CGTTour.lean`. Ce second projet Lake (`conway_cgt_lean/`, toolchain `v4.31.0-rc1`) est\n", - "indépendant de `conway_lean/` (`v4.30.0-rc2`).\n", + "`CGTTour.lean`. Ce second projet Lake (`conway_cgt_lean/`, toolchain `v4.31.0-rc2`) est\n", + "indépendant de `conway_lean/` (`v4.32.1`).\n", "\n", "**Résultats formalises (13 `#check`) :**\n", "\n", @@ -1511,16 +1537,16 @@ "id": "9de9dd11", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T01:04:34.840578Z", - "iopub.status.busy": "2026-06-09T01:04:34.840238Z", - "iopub.status.idle": "2026-06-09T01:04:34.889116Z", - "shell.execute_reply": "2026-06-09T01:04:34.887527Z" + "iopub.execute_input": "2026-09-24T11:44:13.565897Z", + "iopub.status.busy": "2026-09-24T11:44:13.565523Z", + "iopub.status.idle": "2026-09-24T11:44:13.573677Z", + "shell.execute_reply": "2026-09-24T11:44:13.572899Z" }, "papermill": { - "duration": 0.063003, - "end_time": "2026-06-09T01:04:34.890422+00:00", + "duration": 0.015139, + "end_time": "2026-09-24T11:44:13.574713+00:00", "exception": false, - "start_time": "2026-06-09T01:04:34.827419+00:00", + "start_time": "2026-09-24T11:44:13.559574+00:00", "status": "completed" }, "tags": [] @@ -1530,23 +1556,23 @@ "name": "stdout", "output_type": "stream", "text": [ - "=== conway_cgt_lean/CGTTour.lean (169 lignes, sorry = 0) ===\n", + "=== conway_cgt_lean/CGTTour.lean (173 lignes, sorry = 0) ===\n", "Projet Lean (WSL) : MyIA.AI.Notebooks/GameTheory/conway_cgt_lean\n", - "Toolchain : leanprover/lean4:v4.31.0-rc1\n", + "Toolchain : leanprover/lean4:v4.31.0-rc2\n", "Dependance : vihdzp/combinatorial-games (Apache-2.0)\n", "\n", - " # 1 #check @Game.mk -- IGame → Game (quotient map)\n", + " # 1 #check @Game.mk -- IGame → Game (application du quotient)\n", " # 2 #check (inferInstance : AddCommGroupWithOne Game)\n", " # 3 #check (inferInstance : PartialOrder Game)\n", " # 4 #check @Surreal.mk -- IGame → [Numeric] → Surreal\n", - " # 5 #check (inferInstance : LinearOrder Surreal) -- Total order on surreals\n", - " # 6 #check @IGame.Fits.equiv_of_forall_not_fits -- Simplicity theorem\n", + " # 5 #check (inferInstance : LinearOrder Surreal) -- Ordre total sur les surréels\n", + " # 6 #check @IGame.Fits.equiv_of_forall_not_fits -- Théorème de simplicité\n", " # 7 #check (inferInstance : CommRing Surreal)\n", " # 8 #check (inferInstance : LinearOrder Surreal)\n", - " # 9 #check @Dyadic.toIGame -- Dyadic rational → IGame embedding\n", + " # 9 #check @Dyadic.toIGame -- Plongement Rationnel dyadique → IGame\n", " #10 #check @NatOrdinal.toSurreal -- NatOrdinal ↪o Surreal\n", - " #11 #check @Nimber.add_def -- mex definition of nim addition\n", - " #12 #check @Nimber.exists_of_lt_add -- converse: every smaller value is reached\n", + " #11 #check @Nimber.add_def -- Définition de l'addition de nim par mex\n", + " #12 #check @Nimber.exists_of_lt_add -- Réciproque : toute valeur plus petite est atteinte\n", " #13 #check (inferInstance : Field Nimber)\n", "\n", "Total : 13 declarations #check, 0 sorry.\n", @@ -1603,16 +1629,16 @@ "id": "6aef8e25", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T01:04:34.913207Z", - "iopub.status.busy": "2026-06-09T01:04:34.912593Z", - "iopub.status.idle": "2026-06-09T01:29:34.946000Z", - "shell.execute_reply": "2026-06-09T01:29:34.944358Z" + "iopub.execute_input": "2026-09-24T11:44:13.586973Z", + "iopub.status.busy": "2026-09-24T11:44:13.586719Z", + "iopub.status.idle": "2026-09-24T12:09:13.635065Z", + "shell.execute_reply": "2026-09-24T12:09:13.632470Z" }, "papermill": { - "duration": 1500.05759, - "end_time": "2026-06-09T01:29:34.958352+00:00", + "duration": 1500.071298, + "end_time": "2026-09-24T12:09:13.651492+00:00", "exception": false, - "start_time": "2026-06-09T01:04:34.900762+00:00", + "start_time": "2026-09-24T11:44:13.580194+00:00", "status": "completed" }, "tags": [] @@ -1670,10 +1696,10 @@ "id": "5fd82776", "metadata": { "papermill": { - "duration": 0.010655, - "end_time": "2026-06-09T01:29:34.981553+00:00", + "duration": 0.008921, + "end_time": "2026-09-24T12:09:13.671156+00:00", "exception": false, - "start_time": "2026-06-09T01:29:34.970898+00:00", + "start_time": "2026-09-24T12:09:13.662235+00:00", "status": "completed" }, "tags": [] @@ -1691,10 +1717,10 @@ "id": "d9a4f803", "metadata": { "papermill": { - "duration": 0.010135, - "end_time": "2026-06-09T01:29:35.002101+00:00", + "duration": 0.008246, + "end_time": "2026-09-24T12:09:13.687555+00:00", "exception": false, - "start_time": "2026-06-09T01:29:34.991966+00:00", + "start_time": "2026-09-24T12:09:13.679309+00:00", "status": "completed" }, "tags": [] @@ -1715,17 +1741,17 @@ "id": "398b6794", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T01:29:35.024883Z", - "iopub.status.busy": "2026-06-09T01:29:35.024333Z", - "iopub.status.idle": "2026-06-09T01:29:35.033151Z", - "shell.execute_reply": "2026-06-09T01:29:35.031607Z" + "iopub.execute_input": "2026-09-24T12:09:13.706438Z", + "iopub.status.busy": "2026-09-24T12:09:13.705870Z", + "iopub.status.idle": "2026-09-24T12:09:13.718458Z", + "shell.execute_reply": "2026-09-24T12:09:13.717115Z" }, "id": "ex1-nim", "papermill": { - "duration": 0.021928, - "end_time": "2026-06-09T01:29:35.034396+00:00", + "duration": 0.025233, + "end_time": "2026-09-24T12:09:13.719608+00:00", "exception": false, - "start_time": "2026-06-09T01:29:35.012468+00:00", + "start_time": "2026-09-24T12:09:13.694375+00:00", "status": "completed" }, "tags": [] @@ -1765,10 +1791,10 @@ "id": "85643da3", "metadata": { "papermill": { - "duration": 0.009696, - "end_time": "2026-06-09T01:29:35.054021+00:00", + "duration": 0.008248, + "end_time": "2026-09-24T12:09:13.734539+00:00", "exception": false, - "start_time": "2026-06-09T01:29:35.044325+00:00", + "start_time": "2026-09-24T12:09:13.726291+00:00", "status": "completed" }, "tags": [] @@ -1789,17 +1815,17 @@ "id": "1bdf827e", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T01:29:35.079143Z", - "iopub.status.busy": "2026-06-09T01:29:35.078234Z", - "iopub.status.idle": "2026-06-09T01:29:35.087515Z", - "shell.execute_reply": "2026-06-09T01:29:35.085747Z" + "iopub.execute_input": "2026-09-24T12:09:13.753638Z", + "iopub.status.busy": "2026-09-24T12:09:13.753264Z", + "iopub.status.idle": "2026-09-24T12:09:13.764165Z", + "shell.execute_reply": "2026-09-24T12:09:13.762908Z" }, "id": "ex2-looksay", "papermill": { - "duration": 0.024236, - "end_time": "2026-06-09T01:29:35.088733+00:00", + "duration": 0.023084, + "end_time": "2026-09-24T12:09:13.765166+00:00", "exception": false, - "start_time": "2026-06-09T01:29:35.064497+00:00", + "start_time": "2026-09-24T12:09:13.742082+00:00", "status": "completed" }, "tags": [] @@ -1842,10 +1868,10 @@ "id": "fd2a5231", "metadata": { "papermill": { - "duration": 0.011774, - "end_time": "2026-06-09T01:29:35.111587+00:00", + "duration": 0.009047, + "end_time": "2026-09-24T12:09:13.784394+00:00", "exception": false, - "start_time": "2026-06-09T01:29:35.099813+00:00", + "start_time": "2026-09-24T12:09:13.775347+00:00", "status": "completed" }, "tags": [] @@ -1867,17 +1893,17 @@ "id": "2eae064d", "metadata": { "execution": { - "iopub.execute_input": "2026-06-09T01:29:35.139015Z", - "iopub.status.busy": "2026-06-09T01:29:35.138435Z", - "iopub.status.idle": "2026-06-09T01:29:35.146473Z", - "shell.execute_reply": "2026-06-09T01:29:35.144866Z" + "iopub.execute_input": "2026-09-24T12:09:13.816180Z", + "iopub.status.busy": "2026-09-24T12:09:13.815812Z", + "iopub.status.idle": "2026-09-24T12:09:13.875496Z", + "shell.execute_reply": "2026-09-24T12:09:13.856678Z" }, "id": "ex3-angel", "papermill": { - "duration": 0.024334, - "end_time": "2026-06-09T01:29:35.147790+00:00", + "duration": 0.086512, + "end_time": "2026-09-24T12:09:13.877740+00:00", "exception": false, - "start_time": "2026-06-09T01:29:35.123456+00:00", + "start_time": "2026-09-24T12:09:13.791228+00:00", "status": "completed" }, "tags": [] @@ -1911,10 +1937,10 @@ "id": "7d2c357f", "metadata": { "papermill": { - "duration": 0.011507, - "end_time": "2026-06-09T01:29:35.170607+00:00", + "duration": 0.010365, + "end_time": "2026-09-24T12:09:13.900040+00:00", "exception": false, - "start_time": "2026-06-09T01:29:35.159100+00:00", + "start_time": "2026-09-24T12:09:13.889675+00:00", "status": "completed" }, "tags": [] @@ -1950,22 +1976,22 @@ ], "metadata": { "cost": { - "api_usd_est": 0.0, "api_provider": "none", - "qcc_tokens_est": 0, + "api_usd_est": 0.0, + "cpu_min": 2, + "external_account": false, + "free_alternative": "self", "gpu_min": 0, "gpu_required": false, - "vram_gb": 0, - "vram_tier": "none", + "metadata_written": "2026-08-03", "network": true, - "external_account": false, - "free_alternative": "self", + "notes": "Conway biography + Lean formal math (Game of Life, surreal numbers) via lake build. Deterministic. No LLM, no GPU. Network=toolchain fetch.", + "qcc_tokens_est": 0, "reduced_pedagogical": false, "reproducibility": "HIGH", - "metadata_written": "2026-08-03", "validator": "check_cost_metadata.py", - "cpu_min": 2, - "notes": "Conway biography + Lean formal math (Game of Life, surreal numbers) via lake build. Deterministic. No LLM, no GPU. Network=toolchain fetch." + "vram_gb": 0, + "vram_tier": "none" }, "kernelspec": { "display_name": "Python 3 (ipykernel)", @@ -1982,7 +2008,19 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.13.12" + "version": "3.13.7" + }, + "papermill": { + "default_parameters": {}, + "duration": 1828.573144, + "end_time": "2026-09-24T12:09:14.632790+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "Lean-16a-Conway-Man-and-Work.ipynb", + "output_path": "Lean-16a-Conway-Man-and-Work.ipynb", + "parameters": {}, + "start_time": "2026-09-24T11:38:46.059646+00:00", + "version": "2.7.0" } }, "nbformat": 4,