{ "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 }