Blame for code/notebooks/0302-dependent-types.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "00a22d32",
   "metadata": {},
   "source": [
    "# 0302 - Dependent type theory: the minimum for reading Mathlib statements\n",
    "\n",
    "Scratch-pad for note `0302 - Dependent Types.pdf`. Naive first, better second, assert agreement.\n",
    "\n",
    "1. **Universe of a Pi type.** Naive: Python function `imax`-rule. Check against what Lean's kernel says for 10 types.\n",
    "2. **Decidability.** Naive: Python brute force over the bound. Efficient: Lean `decide` (kernel/VM evaluation of the\n",
    "   `Decidable` instance). Assert the Booleans agree on 12 bounded statements; show where no instance exists.\n",
    "3. **Ten miniF2F statements decoded.** Lean prints the elaborated Pi-telescope; Python (exact `Fraction`/big-int arithmetic or\n",
    "   fp64) shows the hypotheses are satisfiable (non-vacuous) and the conclusion holds at witnesses.\n",
    "4. **Elaboration traps** (truncated subtraction, floor division, casts, `autoImplicit`), Lean vs a Python model of ℕ.\n",
    "\n",
    "No GPU (`CUDA_VISIBLE_DEVICES` cleared). Lean: ONE worker through `align.verify.lean`, nice 15."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "fa7036cc",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2026-10-14T09:54:20.065314Z",
     "iopub.status.busy": "2026-10-14T09:54:20.065161Z",
     "iopub.status.idle": "2026-10-14T09:54:24.370858Z",
     "shell.execute_reply": "2026-10-14T09:54:24.370025Z"
    }
   },
   "outputs": [],
   "source": [
    "import os\n",
    "os.environ[\"CUDA_VISIBLE_DEVICES\"] = \"\"\n",
    "import sys, re, json, math, random, itertools, time\n",
    "from fractions import Fraction\n",
    "sys.path.insert(0, os.path.abspath('.'))\n",
    "from _lean_helper import Lean, HEADER\n",
    "MINIF2F_HEADER = \"import Mathlib\\nimport Aesop\\n\\nset_option maxHeartbeats 400000\\n\\nopen BigOperators Real Nat Topology Rat\\n\"\n",
    "L = Lean(MINIF2F_HEADER)\n",
    "\n",
    "def lean_msgs(code, keep=False, timeout=300):\n",
    "    r = L.run(code, timeout=timeout, keep=keep)\n",
    "    return r.get('messages', []), r"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6bd9c629",
   "metadata": {},
   "source": [
    "## 1. The sort of a Pi type: `Sort (imax u v)`\n",
    "Rule: if `A : Sort u` and `B x : Sort v` for `x : A` then `(x : A) → B x : Sort (imax u v)` where\n",
    "`imax u 0 = 0` and `imax u v = max u v` for `v > 0`. So a Pi into `Prop` is a `Prop` whatever the domain (impredicativity)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "a0d26ffc",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2026-10-14T09:54:24.373206Z",
     "iopub.status.busy": "2026-10-14T09:54:24.373041Z",
     "iopub.status.idle": "2026-10-14T09:54:24.406046Z",
     "shell.execute_reply": "2026-10-14T09:54:24.405001Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Pi type                      imax rule  Lean\n",
      "∀ n : ℕ, n = n               Prop       Prop\n",
      "ℕ → ℕ                        Type       Type\n",
      "(n : ℕ) → Fin n              Type       Type\n",
      "∀ p : Prop, p → p            Prop       Prop\n",
      "(α : Type) → α → α           Type 1     Type 1\n",
      "(α : Type) → Prop            Type 1     Type 1\n",
      "Prop → Prop                  Type       Type\n",
      "∀ α : Type, α = α            Prop       Prop\n",
      "(α : Type 1) → α → α         Type 2     Type 2\n",
      "ℕ → Prop                     Type       Type\n",
      "imax rule agrees with the kernel on all 10 types.\n"
     ]
    }
   ],
   "source": [
    "def imax(u, v): return 0 if v == 0 else max(u, v)\n",
    "def sort_name(l): return 'Prop' if l == 0 else ('Type' if l == 1 else f'Type {l-1}')\n",
    "\n",
    "# (lean source of the Pi type, level u of the domain's sort, level v of the codomain's sort)\n",
    "PI_TABLE = [\n",
    "  (\"∀ n : ℕ, n = n\",              1, 0),   # ℕ : Type = Sort 1 ; n = n : Prop = Sort 0\n",
    "  (\"ℕ → ℕ\",                       1, 1),\n",
    "  (\"(n : ℕ) → Fin n\",             1, 1),\n",
    "  (\"∀ p : Prop, p → p\",           1, 0),   # Prop : Type = Sort 1 ; p → p : Prop\n",
    "  (\"(α : Type) → α → α\",          2, 1),   # Type : Type 1 = Sort 2 ; α → α : Type = Sort 1\n",
    "  (\"(α : Type) → Prop\",           2, 1),   # Prop : Type = Sort 1\n",
    "  (\"Prop → Prop\",                 1, 1),\n",
    "  (\"∀ α : Type, α = α\",           2, 0),\n",
    "  (\"(α : Type 1) → α → α\",        3, 2),   # Type 1 : Sort 3 ; α → α : Sort 2\n",
    "  (\"ℕ → Prop\",                    1, 1),\n",
    "]\n",
    "rows = []\n",
    "for src, u, v in PI_TABLE:\n",
    "    msgs, _ = lean_msgs(f\"#check ({src})\")\n",
    "    data = msgs[0]['data']\n",
    "    m = re.search(r\": (Prop|Type\\*?|Type \\d+|Sort [^\\n]*)\\s*$\", data.strip().split('\\n')[-1])\n",
    "    lean_sort = m.group(1) if m else data\n",
    "    pred = sort_name(imax(u, v))\n",
    "    rows.append((src, pred, lean_sort))\n",
    "    assert pred == lean_sort, (src, pred, lean_sort)\n",
    "print(f'{\"Pi type\":28s} {\"imax rule\":10s} Lean')\n",
    "for r_ in rows: print(f'{r_[0]:28s} {r_[1]:10s} {r_[2]}')\n",
    "print('imax rule agrees with the kernel on all', len(rows), 'types.')"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f2877b3a",
   "metadata": {},
   "source": [
    "## 2. Decidability: `Decidable p` is data; `decide` runs it\n",
    "`class Decidable (p : Prop) : Type | isFalse (h : ¬p) | isTrue (h : p)`. `decide p` is `match inst with | isTrue _ => true | isFalse _ => false`.\n",
    "Soundness: `of_decide_eq_true : decide p = true → p` (cases on the instance). The tactic builds `of_decide_eq_true (Eq.refl true)`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "f6a87131",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2026-10-14T09:54:24.407763Z",
     "iopub.status.busy": "2026-10-14T09:54:24.407583Z",
     "iopub.status.idle": "2026-10-14T09:54:24.427808Z",
     "shell.execute_reply": "2026-10-14T09:54:24.427297Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "@of_decide_eq_true : ∀ {p : Prop} [inst : Decidable p], decide p = true → p\n",
      "inductive Decidable : Prop → Type\n",
      "number of parameters: 1\n",
      "constructors:\n",
      "Decidable.isFalse : {p : Prop} → ¬p → Decidable p\n",
      "Decidable.isTrue : {p : Prop} → p → Decidable p\n",
      "theorem two_plus_two : 2 + 2 = 4 :=\n",
      "of_decide_eq_true (Eq.refl true)\n",
      "'two_plus_two' does not depend on any axioms\n"
     ]
    }
   ],
   "source": [
    "msgs, _ = lean_msgs(\"#check @of_decide_eq_true\\n#print Decidable\\ntheorem two_plus_two : 2 + 2 = 4 := by decide\\n#print two_plus_two\\n#print axioms two_plus_two\", keep=True)\n",
    "for m in msgs: print(m['data'])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "357adce9",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2026-10-14T09:54:24.433916Z",
     "iopub.status.busy": "2026-10-14T09:54:24.433656Z",
     "iopub.status.idle": "2026-10-14T09:54:25.615319Z",
     "shell.execute_reply": "2026-10-14T09:54:25.614598Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- Nat.Prime is decidable only via a *chosen* algorithm; two instances exist (the default is chosen by priority) ---\n",
      "decidablePrime 7\n",
      "decidablePrime1 7\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "python  lean   statement\n",
      "True    true   ∀ n < 50, n * n % 4 ≠ 2\n",
      "True    true   ∃ n < 100, n * n = 2209\n",
      "True    true   ∀ a < 20, ∀ b < 20, a * b = b * a\n",
      "True    true   ∀ n < (40 : ℕ), Nat.Prime (n * n + n + 41)\n",
      "False   false  ∀ n < (41 : ℕ), Nat.Prime (n * n + n + 41)\n",
      "True    true   ∀ n < 100, n ^ 3 % 7 = 0 ∨ n ^ 3 % 7 = 1 ∨ n ^ 3 % 7 = 6\n",
      "False   false  ∃ x : Fin 61, ∃ y : Fin 61, 4 * (((x : ℕ) : ℤ) - 30) ^ 3 - 7 * (((y : ℕ) : ℤ) - 30) ^ 3 = 2003\n",
      "False   false  ∀ a < 10, ∀ b < 10, a - b + b = a\n",
      "True    true   ∀ a < 10, ∀ b < 10, (a + b) / 2 * 2 ≤ a + b\n",
      "False   false  ∃ n < 10, 18 ∣ 3740 + n ∧ n ≠ 4\n",
      "True    true   ∀ n < 30, 2 ^ n % 3 = if n % 2 = 0 then 1 else 2\n",
      "True    true   ∃ n < 100, n % 3 = 2 ∧ n % 5 = 3 ∧ n % 7 = 2\n",
      "python brute force == Lean decide on 12/12\n"
     ]
    }
   ],
   "source": [
    "# 12 bounded statements: (python oracle, lean statement)\n",
    "def prime(n):\n",
    "    return n >= 2 and all(n % d for d in range(2, int(n ** .5) + 1))\n",
    "def nsub(a, b): return max(0, a - b)          # Lean ℕ subtraction is truncated\n",
    "CASES = [\n",
    " (lambda: all(n*n % 4 != 2 for n in range(50)),                         \"∀ n < 50, n * n % 4 ≠ 2\"),\n",
    " (lambda: any(n*n == 2209 for n in range(100)),                         \"∃ n < 100, n * n = 2209\"),\n",
    " (lambda: all(a*b == b*a for a in range(20) for b in range(20)),        \"∀ a < 20, ∀ b < 20, a * b = b * a\"),\n",
    " (lambda: all(prime(n*n+n+41) for n in range(40)),                      \"∀ n < (40 : ℕ), Nat.Prime (n * n + n + 41)\"),\n",
    " (lambda: all(prime(n*n+n+41) for n in range(41)),                      \"∀ n < (41 : ℕ), Nat.Prime (n * n + n + 41)\"),\n",
    " (lambda: all(n**3 % 7 in (0, 1, 6) for n in range(100)),               \"∀ n < 100, n ^ 3 % 7 = 0 ∨ n ^ 3 % 7 = 1 ∨ n ^ 3 % 7 = 6\"),\n",
    " (lambda: any(4*x**3 - 7*y**3 == 2003 for x in range(-30, 31) for y in range(-30, 31)),\n",
    "                                                                        \"∃ x : Fin 61, ∃ y : Fin 61, 4 * (((x : ℕ) : ℤ) - 30) ^ 3 - 7 * (((y : ℕ) : ℤ) - 30) ^ 3 = 2003\"),\n",
    " (lambda: all(nsub(a, b) + b == a for a in range(10) for b in range(10)),   \"∀ a < 10, ∀ b < 10, a - b + b = a\"),\n",
    " (lambda: all((a + b) // 2 * 2 <= a + b for a in range(10) for b in range(10)), \"∀ a < 10, ∀ b < 10, (a + b) / 2 * 2 ≤ a + b\"),\n",
    " (lambda: any((3740 + n) % 18 == 0 and n != 4 for n in range(10)),      \"∃ n < 10, 18 ∣ 3740 + n ∧ n ≠ 4\"),\n",
    " (lambda: all(pow(2, n) % 3 == (1 if n % 2 == 0 else 2) for n in range(30)), \"∀ n < 30, 2 ^ n % 3 = if n % 2 = 0 then 1 else 2\"),\n",
    " (lambda: any(n % 3 == 2 and n % 5 == 3 and n % 7 == 2 for n in range(100)), \"∃ n < 100, n % 3 = 2 ∧ n % 5 = 3 ∧ n % 7 = 2\"),\n",
    "]\n",
    "print('--- Nat.Prime is decidable only via a *chosen* algorithm; two instances exist (the default is chosen by priority) ---')\n",
    "for m in lean_msgs(\"#synth Decidable (Nat.Prime 7)\")[0]: print(m['data'][:160])\n",
    "lean_msgs(\"attribute [instance] Nat.decidablePrime1\", keep=True)      # opt in to the trial-division instance (needed below for bounded foralls)\n",
    "for m in lean_msgs(\"#synth Decidable (Nat.Prime 7)\")[0]: print(m['data'][:160])\n",
    "code = \"\\n\".join(f\"#eval decide ({s})\" for _, s in CASES)\n",
    "msgs, _ = lean_msgs(code)\n",
    "by_line = {m['pos']['line']: m['data'].strip() for m in msgs}\n",
    "print(f'{\"python\":7s} {\"lean\":6s} statement')\n",
    "agree = 0\n",
    "for i, (fn, s) in enumerate(CASES, start=1):\n",
    "    py = fn(); ln = by_line.get(i)\n",
    "    assert ln in ('true', 'false'), (s, ln)\n",
    "    assert (ln == 'true') == py, (s, py, ln)\n",
    "    agree += 1\n",
    "    print(f'{str(py):7s} {ln:6s} {s}')\n",
    "print(f'python brute force == Lean decide on {agree}/{len(CASES)}')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "c58167d4",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2026-10-14T09:54:25.617088Z",
     "iopub.status.busy": "2026-10-14T09:54:25.616927Z",
     "iopub.status.idle": "2026-10-14T09:54:25.737634Z",
     "shell.execute_reply": "2026-10-14T09:54:25.736825Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "--- elaboration order matters: the same statement without the type ascription has no instance (n : ?α is still a metavariable) ---\n",
      "failed to synthesize\n",
      "  Decidable (∀ n < 40, (n * n + n + 41).Prime)\n",
      "use `set_option diagnostics true` to get diagnostic information\n",
      "--- no instance: unbounded quantifier over ℕ ---\n",
      "failed to synthesize\n",
      "  Decidable (∀ (n : ℕ), n < 5 ∨ 5 ≤ n)\n",
      "use `set_option diagnostics true` to get diagnostic information\n",
      "--- no computable instance: equality on ℝ ---\n",
      "tactic 'decide' failed for proposition\n",
      "  2 + 2 = 4\n",
      "since its 'Decidable' instance reduced to\n",
      "  Classical.choice ⋯\n",
      "rather than to the 'isTrue' constructor.\n",
      "--- but a *closed* bounded one is fine, and the real statements with binders are not decidable props at all ---\n",
      "decidableBallLT 10 fun n a => n * n < 100\n",
      "failed to synthesize\n",
      "  Decidable (∀ (x : ℝ), x ^ 2 ≥ 0)\n",
      "use `set_option diagnostics true` to get diagnostic information\n"
     ]
    }
   ],
   "source": [
    "print('--- elaboration order matters: the same statement without the type ascription has no instance (n : ?α is still a metavariable) ---')\n",
    "for m in lean_msgs(\"#eval decide (∀ n < 40, Nat.Prime (n * n + n + 41))\")[0]: print(m['data'][:160])\n",
    "print('--- no instance: unbounded quantifier over ℕ ---')\n",
    "for m in lean_msgs(\"example : ∀ n : ℕ, n < 5 ∨ 5 ≤ n := by decide\")[0]: print(m['data'][:400])\n",
    "print('--- no computable instance: equality on ℝ ---')\n",
    "for m in lean_msgs(\"example : (2 : ℝ) + 2 = 4 := by decide\")[0]: print(m['data'][:400])\n",
    "print('--- but a *closed* bounded one is fine, and the real statements with binders are not decidable props at all ---')\n",
    "for m in lean_msgs(\"#synth Decidable (∀ n < 10, n * n < 100)\")[0]: print(m['data'][:200])\n",
    "for m in lean_msgs(\"#synth Decidable (∀ x : ℝ, x ^ 2 ≥ 0)\")[0]: print(m['data'][:200])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c172fa47",
   "metadata": {},
   "source": [
    "## 3. Ten miniF2F statements decoded\n",
    "Source: `p2_runs/r1_baseline/minif2f.jsonl` (the 244 miniF2F test statements this repo evaluates on, Lean 4.9.0-rc1 + Mathlib pin).\n",
    "For each: (a) Lean's own elaborated Pi-telescope (`#check @name`), its sort, and `decide`-ability of the closed ones;\n",
    "(b) a Python witness check that the hypotheses are satisfiable and the conclusion holds there (non-vacuity), exact arithmetic where possible."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "f06bbc76",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2026-10-14T09:54:25.739310Z",
     "iopub.status.busy": "2026-10-14T09:54:25.739151Z",
     "iopub.status.idle": "2026-10-14T09:54:26.102413Z",
     "shell.execute_reply": "2026-10-14T09:54:26.101621Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "====================================================================================================\n",
      "mathd_algebra_478\n",
      "mathd_algebra_478 : ∀ (b h v : ℝ), 0 < b ∧ 0 < h ∧ 0 < v → v = 1 / 3 * (b * h) → b = 30 → h = 13 / 2 → v = 65\n",
      "binders=7 sort=Prop\n",
      "====================================================================================================\n",
      "numbertheory_4x3m7y3neq2003\n",
      "numbertheory_4x3m7y3neq2003 : ∀ (x y : ℤ), 4 * x ^ 3 - 7 * y ^ 3 ≠ 2003\n",
      "binders=2 sort=Prop\n",
      "====================================================================================================\n",
      "aime_1983_p1\n",
      "aime_1983_p1 : ∀ (x y z w : ℕ), 1 < x ∧ 1 < y ∧ 1 < z → 0 ≤ w → (↑w).log / (↑x).log = 24 → (↑w).log / (↑y).log = 40 → (↑w).log / (↑x * ↑y * ↑z).log = 12 → (↑w).log / (↑z).log = 60\n",
      "binders=9 sort=Prop\n",
      "====================================================================================================\n",
      "amc12_2001_p5\n",
      "amc12_2001_p5 : (Finset.filter (fun x => ¬Even x) (Finset.range 10000)).prod id = 10000! / (2 ^ 5000 * 5000!)\n",
      "binders=0 sort=Prop\n",
      "====================================================================================================\n",
      "mathd_numbertheory_3\n",
      "mathd_numbertheory_3 : (∑ x ∈ Finset.range 10, (x + 1) ^ 2) % 10 = 5\n",
      "binders=0 sort=Prop\n",
      "====================================================================================================\n",
      "imo_1969_p2\n",
      "imo_1969_p2 : ∀ (m n : ℝ) (k : ℕ) (a : ℕ → ℝ) (y : ℝ → ℝ), 0 < k → (∀ (x : ℝ), y x = ∑ i ∈ Finset.range k, (a i + x).cos / 2 ^ i) → y m = 0 → y n = 0 → ∃ t, m - n = ↑t * π\n",
      "binders=9 sort=Prop\n",
      "====================================================================================================\n",
      "mathd_algebra_209\n",
      "mathd_algebra_209 : ∀ (σ : ℝ ≃ ℝ), σ.invFun 2 = 10 → σ.invFun 10 = 1 → σ.invFun 1 = 2 → σ.toFun (σ.toFun 10) = 1\n",
      "binders=4 sort=Prop\n",
      "====================================================================================================\n",
      "mathd_numbertheory_1124\n",
      "mathd_numbertheory_1124 : ∀ n ≤ 9, 18 ∣ 374 * 10 + n → n = 4\n",
      "binders=3 sort=Prop\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "====================================================================================================\n",
      "imo_1983_p6\n",
      "imo_1983_p6 : ∀ (a b c : ℝ), 0 < a ∧ 0 < b ∧ 0 < c → c < a + b → b < a + c → a < b + c → 0 ≤ a ^ 2 * b * (a - b) + b ^ 2 * c * (b - c) + c ^ 2 * a * (c - a)\n",
      "binders=7 sort=Prop\n",
      "====================================================================================================\n",
      "mathd_algebra_33\n",
      "mathd_algebra_33 : ∀ (x y z : ℝ), x ≠ 0 → 2 * x = 5 * y → 7 * y = 10 * z → z / x = 7 / 25\n",
      "binders=6 sort=Prop\n"
     ]
    }
   ],
   "source": [
    "PICK = ['mathd_algebra_478', 'numbertheory_4x3m7y3neq2003', 'aime_1983_p1', 'amc12_2001_p5', 'mathd_numbertheory_3',\n",
    "        'imo_1969_p2', 'mathd_algebra_209', 'mathd_numbertheory_1124', 'imo_1983_p6', 'mathd_algebra_33']\n",
    "rows = {}\n",
    "for l_ in open('/apps/development/rlhf/p2_runs/r1_baseline/minif2f.jsonl'):\n",
    "    r_ = json.loads(l_)\n",
    "    if r_['problem_id'] in PICK: rows[r_['problem_id']] = r_\n",
    "assert set(rows) == set(PICK)\n",
    "\n",
    "SORT_ELAB = r'''\n",
    "open Lean Meta Elab Command in\n",
    "elab \"#sort_of \" id:ident : command => do\n",
    "  let env ← getEnv\n",
    "  match env.find? id.getId with\n",
    "  | none => throwError \"unknown\"\n",
    "  | some ci => liftTermElabM do\n",
    "      let s ← inferType ci.type\n",
    "      let nb := (← forallTelescope ci.type fun xs _ => pure xs.size)\n",
    "      logInfo m!\"binders={nb} sort={← whnf s}\"\n",
    "'''\n",
    "L.run(SORT_ELAB, keep=True)\n",
    "\n",
    "decoded = {}\n",
    "for pid in PICK:\n",
    "    st = rows[pid]['formal_statement']\n",
    "    thm = st[st.index('/--'):]                                   # docstring + theorem ... := by sorry\n",
    "    rest = thm\n",
    "    msgs, r = lean_msgs(rest + f\"\\n#check @{pid}\\n#sort_of {pid}\", timeout=300)\n",
    "    out = [m['data'] for m in msgs if m['severity'] == 'info']\n",
    "    errs = [m['data'] for m in msgs if m['severity'] == 'error']\n",
    "    assert not errs, errs\n",
    "    decoded[pid] = out\n",
    "    print('=' * 100); print(pid)\n",
    "    print(re.sub(r'\\n\\s+', ' ', out[0]))\n",
    "    print(out[1])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2d1b76ed",
   "metadata": {},
   "source": [
    "Closed statements (no binders) are plain `Prop`s with a `Decidable` instance: Lean can *evaluate* them."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "852923ed",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2026-10-14T09:54:26.104415Z",
     "iopub.status.busy": "2026-10-14T09:54:26.104258Z",
     "iopub.status.idle": "2026-10-14T09:54:26.288412Z",
     "shell.execute_reply": "2026-10-14T09:54:26.287495Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "amc12_2001_p5 -> ['instDecidableEqNat ((Finset.filter (fun x => ¬Even x) (Finset.range 10000)).prod', 'true']\n",
      "mathd_numbertheory_3 -> ['instDecidableEqNat ((∑ x ∈ Finset.range 10, (x + 1) ^ 2) % 10) 5', 'true']\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\"'nt3' depends on axioms: [propext, Quot.sound]\"]\n"
     ]
    }
   ],
   "source": [
    "for pid in ['amc12_2001_p5', 'mathd_numbertheory_3']:\n",
    "    st = rows[pid]['formal_statement']\n",
    "    body = st.split(f'theorem {pid} :')[1].split(':= by sorry')[0].strip()\n",
    "    msgs, _ = lean_msgs(f\"#synth Decidable ({body})\\n#eval decide ({body})\", timeout=300)\n",
    "    print(pid, '->', [m['data'].strip()[:80] for m in msgs])\n",
    "msgs, _ = lean_msgs(\"theorem nt3 : (∑ x in Finset.range 10, (x + 1) ^ 2) % 10 = 5 := by decide\\n#print axioms nt3\")\n",
    "print([m['data'] for m in msgs])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "b59c7854",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2026-10-14T09:54:26.290114Z",
     "iopub.status.busy": "2026-10-14T09:54:26.289954Z",
     "iopub.status.idle": "2026-10-14T09:54:26.591691Z",
     "shell.execute_reply": "2026-10-14T09:54:26.590442Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "mathd_algebra_478              OK  witness b=30,h=13/2 => v=65 exactly\n",
      "numbertheory_4x3m7y3neq2003    OK  cubes mod 7 = [0, 1, 6]; 4*cubes mod 7 = [0, 3, 4]; 2003 mod 7 = 1 not attained; box [-80,80]^2 empty\n",
      "aime_1983_p1                   OK  fp64 max hypothesis residual 0.00e+00, conclusion residual 0.00e+00; exact: L/(L/12-L/24-L/40)=60\n",
      "amc12_2001_p5                  OK  product of odd numbers < 10000 == 10000!/(2^5000 * 5000!) as big integers; division exact\n",
      "mathd_numbertheory_3           OK  sum = 385, 385 mod 10 = 5\n",
      "imo_1969_p2                    OK  200 random (k,a): y(x)=A cos x - B sin x; zeros m,n: max |y(m)|,|y(n)|,|(m-n)/π - t| = 3.7e-15; |(A,B)| >= 2^(1-k) > 0 in all 200 runs\n",
      "mathd_algebra_209              OK  σ = {10: 2, 1: 10, 2: 1}; σ(σ(10)) = 1\n",
      "mathd_numbertheory_1124        OK  solutions n in 0..9 with 18 | 3740+n: [4]\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "imo_1983_p6                    OK  min over 2e5 random triangles of E/a^4 = 6.588e-08 (>= 0); a=b=c gives exactly 0\n",
      "mathd_algebra_33               OK  x=1,y=2/5,z=7/25: z/x = 7/25 exactly\n",
      "all 10 statements: hypotheses satisfiable (non-vacuous) and conclusion verified at witnesses / exhaustively.\n"
     ]
    }
   ],
   "source": [
    "# ---- (b) Python witness checks, one per statement ----\n",
    "def check_478():\n",
    "    b, h = Fraction(30), Fraction(13, 2)\n",
    "    v = Fraction(1, 3) * (b * h)\n",
    "    assert 0 < b and 0 < h and 0 < v          # hypotheses satisfiable (h₀)\n",
    "    assert v == 65                           # conclusion\n",
    "    return 'witness b=30,h=13/2 => v=65 exactly'\n",
    "\n",
    "def check_4x3m7y3():\n",
    "    cubes = {pow(n, 3, 7) for n in range(7)}\n",
    "    resid = {(4 * c) % 7 for c in cubes}\n",
    "    assert 2003 % 7 == 1 and 1 not in resid  # the real proof: 4x^3 - 7y^3 ≡ 4x^3 (mod 7)\n",
    "    assert not any(4*x**3 - 7*y**3 == 2003 for x in range(-80, 81) for y in range(-80, 81))\n",
    "    return f'cubes mod 7 = {sorted(cubes)}; 4*cubes mod 7 = {sorted(resid)}; 2003 mod 7 = 1 not attained; box [-80,80]^2 empty'\n",
    "\n",
    "def check_aime():\n",
    "    # w = 2^120, x = 2^5, y = 2^3, z = 2^2 : satisfies all three hypotheses; conclusion log_z w = 60\n",
    "    x, y, z, w = 2**5, 2**3, 2**2, 2**120\n",
    "    errs = [abs(math.log(w)/math.log(x) - 24), abs(math.log(w)/math.log(y) - 40), abs(math.log(w)/math.log(x*y*z) - 12)]\n",
    "    concl = abs(math.log(w)/math.log(z) - 60)\n",
    "    assert max(errs) < 1e-12 and concl < 1e-12\n",
    "    Lw = Fraction(120); lz = Lw/12 - Lw/24 - Lw/40      # log z = log(xyz) - log x - log y\n",
    "    assert Lw / lz == 60                                  # exact derivation\n",
    "    return f'fp64 max hypothesis residual {max(errs):.2e}, conclusion residual {concl:.2e}; exact: L/(L/12-L/24-L/40)=60'\n",
    "\n",
    "def check_amc():\n",
    "    prod = 1\n",
    "    for x in range(10000):\n",
    "        if x % 2 == 1: prod *= x\n",
    "    rhs_num = math.factorial(10000); rhs_den = 2**5000 * math.factorial(5000)\n",
    "    assert rhs_num % rhs_den == 0               # the ℕ-division is exact, so truncation plays no role\n",
    "    assert prod == rhs_num // rhs_den\n",
    "    return 'product of odd numbers < 10000 == 10000!/(2^5000 * 5000!) as big integers; division exact'\n",
    "\n",
    "def check_nt3():\n",
    "    s = sum((x + 1) ** 2 for x in range(10)); assert s == 385 and s % 10 == 5\n",
    "    return 'sum = 385, 385 mod 10 = 5'\n",
    "\n",
    "def check_imo69():\n",
    "    random.seed(1); worst = 0.0\n",
    "    for _ in range(200):\n",
    "        k = random.randint(1, 8); a = [random.uniform(-10, 10) for _ in range(k)]\n",
    "        A = sum(math.cos(a[i]) / 2**i for i in range(k)); B = sum(math.sin(a[i]) / 2**i for i in range(k))\n",
    "        x0 = math.atan2(A, B)                      # y(x) = A cos x - B sin x = 0  <=>  x = atan2(A,B) + tπ\n",
    "        y = lambda x: sum(math.cos(a[i] + x) / 2**i for i in range(k))\n",
    "        m, n = x0 + 3 * math.pi, x0 - 2 * math.pi\n",
    "        worst = max(worst, abs(y(m)), abs(y(n)), abs((m - n) / math.pi - 5))\n",
    "        assert math.hypot(A, B) >= 2.0 ** (1 - k) - 1e-12     # |sum_i e^{i a_i} 2^-i| >= 1 - sum_{i=1}^{k-1} 2^-i = 2^(1-k) > 0 (FINITE sum)\n",
    "    assert worst < 1e-12\n",
    "    return f'200 random (k,a): y(x)=A cos x - B sin x; zeros m,n: max |y(m)|,|y(n)|,|(m-n)/π - t| = {worst:.1e}; |(A,B)| >= 2^(1-k) > 0 in all 200 runs'\n",
    "\n",
    "def check_209():\n",
    "    inv = {2: 10, 10: 1, 1: 2}                    # σ.2 = invFun\n",
    "    sigma = {v: k for k, v in inv.items()}\n",
    "    assert sigma[sigma[10]] == 1\n",
    "    return f'σ = {sigma}; σ(σ(10)) = {sigma[sigma[10]]}'\n",
    "\n",
    "def check_1124():\n",
    "    sol = [n for n in range(10) if (374 * 10 + n) % 18 == 0]\n",
    "    assert sol == [4]\n",
    "    return f'solutions n in 0..9 with 18 | 3740+n: {sol}'\n",
    "\n",
    "def check_1983():\n",
    "    random.seed(2); worst = float('inf')\n",
    "    for _ in range(200000):\n",
    "        x, y, z = (random.uniform(1e-3, 10) for _ in range(3))      # Ravi: a=y+z, b=z+x, c=x+y  => triangle inequalities hold\n",
    "        a, b, c = y + z, z + x, x + y\n",
    "        val = a*a*b*(a-b) + b*b*c*(b-c) + c*c*a*(c-a)\n",
    "        worst = min(worst, val / (a**4))                            # scale-free\n",
    "    assert worst > -1e-12\n",
    "    t = Fraction(7); assert t*t*t*(t-t) * 3 == 0\n",
    "    return f'min over 2e5 random triangles of E/a^4 = {worst:.3e} (>= 0); a=b=c gives exactly 0'\n",
    "\n",
    "def check_33():\n",
    "    x = Fraction(1); y = 2 * x / 5; z = 7 * y / 10\n",
    "    assert x != 0 and 2*x == 5*y and 7*y == 10*z and z / x == Fraction(7, 25)\n",
    "    return f'x=1,y={y},z={z}: z/x = 7/25 exactly'\n",
    "\n",
    "CHECKS = {'mathd_algebra_478': check_478, 'numbertheory_4x3m7y3neq2003': check_4x3m7y3, 'aime_1983_p1': check_aime,\n",
    "          'amc12_2001_p5': check_amc, 'mathd_numbertheory_3': check_nt3, 'imo_1969_p2': check_imo69,\n",
    "          'mathd_algebra_209': check_209, 'mathd_numbertheory_1124': check_1124, 'imo_1983_p6': check_1983,\n",
    "          'mathd_algebra_33': check_33}\n",
    "for pid in PICK:\n",
    "    print(f'{pid:30s} OK  {CHECKS[pid]()}')\n",
    "print('all 10 statements: hypotheses satisfiable (non-vacuous) and conclusion verified at witnesses / exhaustively.')"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4fadce18",
   "metadata": {},
   "source": [
    "## 3b. Lemma checks (section 3.4 of the note)\n",
    "`(a - b) + b = max a b` on ℕ (exhaustive in a box AND a Lean proof); the Euclidean division law `a = b*(a/b) + a%b, 0 <= a%b < |b|` for Lean's ℤ (exhaustive grid evaluated by Lean); and `x / 0 = 0` on ℝ."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "165b7f70",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2026-10-14T09:54:26.593548Z",
     "iopub.status.busy": "2026-10-14T09:54:26.593364Z",
     "iopub.status.idle": "2026-10-14T09:54:27.071951Z",
     "shell.execute_reply": "2026-10-14T09:54:27.071277Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Lean: a - b + b = max a b proved; 'tsub_add_max' depends on axioms: [propext, Quot.sound] | and the naive \"a - b + b = a\" is refuted at (0,1)\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Lean ℤ: b*(a/b) + a%b = a and 0 <= a%b < |b| on 1464 grid points; Lean (a/b, a%b) == the unique Euclidean (q,r) on all of them; x/0 = 0, x%0 = x\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Lean ℝ: ∀ x, x / 0 = 0 proved (div_zero); 'real_div_zero' depends on axioms: [propext, Classical.choice, Quot.sound]\n"
     ]
    }
   ],
   "source": [
    "\n",
    "# (i) truncated subtraction: (a - b) + b = max a b\n",
    "assert all(max(0, a - b) + b == max(a, b) for a in range(61) for b in range(61))\n",
    "msgs, _ = lean_msgs(\"\"\"\n",
    "theorem tsub_add_max (a b : ℕ) : a - b + b = max a b := by omega\n",
    "#print axioms tsub_add_max\n",
    "theorem tsub_add_false : ¬ (∀ a b : ℕ, a - b + b = a) := fun h => by have := h 0 1; simp at this\n",
    "\"\"\")\n",
    "assert not [m for m in msgs if m['severity'] == 'error'], msgs\n",
    "print('Lean: a - b + b = max a b proved;', [m['data'] for m in msgs if m['severity'] == 'info'][0], '| and the naive \"a - b + b = a\" is refuted at (0,1)')\n",
    "# (ii) Euclidean division law for Int, exhaustive on a grid, evaluated by Lean\n",
    "msgs, _ = lean_msgs(\"\"\"\n",
    "#eval (List.range 61).all fun ai => (List.range 25).all fun bi =>\n",
    "  let a : Int := (ai : Int) - 30\n",
    "  let b : Int := (bi : Int) - 12\n",
    "  b == 0 || ((b * (a / b) + a % b == a) && decide (0 ≤ a % b) && decide (a % b < (b.natAbs : Int)))\n",
    "#eval (List.range 61).all fun ai => (List.range 25).all fun bi => ((ai : Int) - 30) / 0 == 0 && ((ai : Int) - 30) % 0 == (ai : Int) - 30\n",
    "\"\"\")\n",
    "res = [m['data'].strip() for m in msgs if m['severity'] == 'info']\n",
    "assert res == ['true', 'true'], (res, msgs)\n",
    "# the unique (q, r) with a = b q + r, 0 <= r < |b| (Python model) must equal Lean's / and %\n",
    "def euclid(a, b):\n",
    "    r = a % abs(b); q = (a - r) // b; return q, r\n",
    "lean_vals = lean_msgs(\"#eval (List.range 61).bind fun ai => (List.range 25).filterMap fun bi => let a : Int := (ai : Int) - 30; let b : Int := (bi : Int) - 12; if b == 0 then none else some (a / b, a % b)\")[0]\n",
    "import ast\n",
    "lv = ast.literal_eval(lean_vals[0]['data'].replace('(', '(').strip()) if lean_vals and lean_vals[0]['severity'] == 'info' else None\n",
    "pv = [euclid(ai - 30, bi - 12) for ai in range(61) for bi in range(25) if bi != 12]\n",
    "assert lv is not None and [tuple(x) for x in lv] == pv, 'Lean Int / and % differ from the Euclidean (q, r) model'\n",
    "print(f'Lean ℤ: b*(a/b) + a%b = a and 0 <= a%b < |b| on {len(pv)} grid points; Lean (a/b, a%b) == the unique Euclidean (q,r) on all of them; x/0 = 0, x%0 = x')\n",
    "# (iii) x / 0 = 0 on the reals\n",
    "msgs, _ = lean_msgs(\"theorem real_div_zero : ∀ x : ℝ, x / 0 = 0 := fun x => div_zero x\\n#print axioms real_div_zero\")\n",
    "assert not [m for m in msgs if m['severity'] == 'error'], msgs\n",
    "print('Lean ℝ: ∀ x, x / 0 = 0 proved (div_zero);', [m['data'] for m in msgs if m['severity'] == 'info'][0])\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8d2c076e",
   "metadata": {},
   "source": [
    "## 4. Elaboration traps (where a *correct-looking* statement means something else)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "85822ae4",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2026-10-14T09:54:27.074232Z",
     "iopub.status.busy": "2026-10-14T09:54:27.074069Z",
     "iopub.status.idle": "2026-10-14T09:54:27.447944Z",
     "shell.execute_reply": "2026-10-14T09:54:27.447329Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(5 : ℕ) - 7                  = 0\n",
      "(7 : ℕ) / 2                  = 3\n",
      "(7 : ℤ) / (-2)               = -3\n",
      "(-7 : ℤ) / 2                 = -4\n",
      "(-7 : ℤ) % 3                 = 2\n",
      "(((5 : ℕ) - 7 : ℕ) : ℤ)      = 0\n",
      "((5 : ℕ) : ℤ) - 7            = -2\n",
      "((10 : ℕ) - 3) / 2           = 3\n",
      "(2 : ℕ) ^ 3 ^ 2              = 512\n",
      "Lean 7/(-2) = -3  and (-7)/2 = -4 (Euclidean: remainder is always >= 0)\n",
      "--- autoImplicit: a typo silently becomes a new universally-quantified variable ---\n",
      "warning declaration uses 'sorry'\n",
      "info @t_typo : ∀ {xx : ℕ} (x : ℕ), x + 1 > xx\n",
      "--- the same with autoImplicit off: an error, as it should be ---\n",
      "error unknown identifier 'xx'\n"
     ]
    }
   ],
   "source": [
    "TRAPS = [\n",
    " (\"(5 : ℕ) - 7\",           lambda: nsub(5, 7),            \"0\"),\n",
    " (\"(7 : ℕ) / 2\",           lambda: 7 // 2,                \"3\"),\n",
    " (\"(7 : ℤ) / (-2)\",        lambda: 'ediv',                None),\n",
    " (\"(-7 : ℤ) / 2\",          lambda: 'ediv',                None),\n",
    " (\"(-7 : ℤ) % 3\",          lambda: (-7) % 3,              \"2\"),\n",
    " (\"(((5 : ℕ) - 7 : ℕ) : ℤ)\", lambda: nsub(5, 7),          \"0\"),\n",
    " (\"((5 : ℕ) : ℤ) - 7\",     lambda: 5 - 7,                 \"-2\"),\n",
    " (\"((10 : ℕ) - 3) / 2\",    lambda: (10 - 3) // 2,         \"3\"),\n",
    " (\"(2 : ℕ) ^ 3 ^ 2\",       lambda: 2 ** (3 ** 2),         \"512\"),\n",
    "]\n",
    "msgs, _ = lean_msgs(\"\\n\".join(f\"#eval {s}\" for s, _, _ in TRAPS))\n",
    "by_line = {m['pos']['line']: m['data'].strip() for m in msgs}\n",
    "for i, (s, fn, expect) in enumerate(TRAPS, start=1):\n",
    "    got = by_line[i]\n",
    "    if expect is not None:\n",
    "        assert got == expect, (s, got, expect)\n",
    "        py = fn(); assert str(py) == got, (s, py, got)\n",
    "    print(f'{s:28s} = {got}')\n",
    "# Lean's ℤ `/` is Euclidean-style `Int.div` (T-rounding is `Int.tdiv`): -7/2 = -4, 7/(-2) = -3 ; Python's // floors: -7//2 = -4, 7//(-2) = -4\n",
    "print('Lean 7/(-2) =', by_line[3], ' and (-7)/2 =', by_line[4], '(Euclidean: remainder is always >= 0)')\n",
    "assert by_line[4] == '-4' and by_line[3] == '-3'\n",
    "assert (-7) // 2 == -4 and 7 // -2 == -4            # python floors: differs from Lean on 7 / (-2)\n",
    "\n",
    "print('--- autoImplicit: a typo silently becomes a new universally-quantified variable ---')\n",
    "for m in lean_msgs(\"theorem t_typo (x : ℕ) : x + 1 > xx := by sorry\\n#check @t_typo\")[0]: print(m['severity'], m['data'][:300])\n",
    "print('--- the same with autoImplicit off: an error, as it should be ---')\n",
    "for m in lean_msgs(\"set_option autoImplicit false in\\ntheorem t_typo2 (x : ℕ) : x + 1 > xx := by sorry\")[0]: print(m['severity'], m['data'][:200])\n",
    "L.close()"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.12.11"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}