progress

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1

.gitignore

@@ -0,0 +1 @@
+/.lake

Collatz.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Collatz` library.
+-- Import modules here that should be built as part of the library.
+import Collatz.Basic

Collatz/Basic.lean

@@ -0,0 +1,132 @@
+import Mathlib
+
+open Nat
+
+/-- The Collatz function: if n is even, divide by 2; if odd, multiply by 3 and add 1 -/
+def collatz (n : Nat) : Nat :=
+  if n % 2 = 0 then n / 2 else 3 * n + 1
+
+/-- Iterate the Collatz function k times starting from n -/
+def collatzIter (n : Nat) : Nat → Nat
+| 0 => n
+| k+1 => collatz (collatzIter n k)
+
+theorem collatzIter_pos {n k : Nat} (hn : n > 0) : collatzIter n k > 0 := by
+  induction k with
+  | zero => exact hn
+  | succ k ih =>
+    rw [collatzIter, collatz]
+    by_cases h : (collatzIter n k) % 2 = 0
+    · -- Even case
+      rw [if_pos h]
+      rcases Nat.even_iff.mpr h with ⟨m, hm⟩
+      -- Goal: (collatzIter n k)/2 > 0
+      change (collatzIter n k)/2 > 0
+      rw [hm, ←two_mul m]
+      have eq_m : (2 * m) / 2 = m := Nat.mul_div_cancel_left m (by decide)
+      rw [eq_m]
+      cases m with
+      | zero =>
+        -- If m=0, then collatzIter n k = 0 contradicting ih > 0
+        simp at hm
+        rw [hm] at ih
+        exfalso
+        exact Nat.lt_irrefl 0 ih
+      | succ m' =>
+        -- If m>0, then m>0
+        exact Nat.succ_pos m'
+    · -- Odd case
+      rw [if_neg h]
+      exact Nat.succ_pos (3 * (collatzIter n k))
+
+/-- For odd n, collatz n = 3n+1 -/
+theorem odd_step_exact {n : Nat} (hodd : Odd n) :
+  collatz n = 3 * n + 1 := by
+  rw [collatz]
+  have h : n % 2 ≠ 0 := by
+    intro h2
+    have := Nat.even_iff.mpr h2
+    have := Nat.not_even_iff_odd.mpr hodd
+    contradiction
+  rw [if_neg h]
+
+/-- After odd value, next value is even -/
+theorem odd_gives_even {n : Nat} (hodd : Odd n) : Even (collatz n) := by
+  obtain ⟨k, rfl⟩ := hodd
+  rw [collatz]
+  have : (2 * k + 1) % 2 = 1 := by
+    rw [Nat.add_mod, Nat.mul_mod, Nat.mul_comm]
+    simp
+  rw [this]
+  -- Now we have collatz (2*k+1) = if 1=0 then ... else 3*(2*k+1)+1
+  rw [if_neg (by decide)]  -- since 1 = 0 is false
+  -- collatz (2*k+1) is now 3*(2*k+1) + 1
+  use (3*k + 2)
+  -- Now we need to show 3*(2*k+1) + 1 = 2*(3*k+2)
+  ring
+
+/-- For even values, next step = val/2 -/
+theorem even_step_decrease {n k : Nat} (hn : n > 0) (heven : Even (collatzIter n k)) :
+  collatzIter n (k+1) = collatzIter n k / 2 := by
+  rw [collatzIter, collatz]
+  have : (collatzIter n k) % 2 = 0 := Nat.even_iff.mp heven
+  rw [if_pos this]
+
+/-- Between even steps, find a smaller value -/
+theorem bounded_growth_between_even {n : Nat} (hn : n > 0) :
+  ∀ k, Even (collatzIter n k) →
+  ∃ j, j > k ∧ Even (collatzIter n j) ∧ collatzIter n j < collatzIter n k := by
+  intros k heven
+  by_cases h_next_odd : Odd (collatzIter n (k+1))
+  · -- If next is odd, (k+2) is even and smaller
+    have h_even_k2 : Even (collatzIter n (k+2)) := odd_gives_even h_next_odd
+    use k+2
+    constructor; linarith
+    constructor; exact h_even_k2
+    let val := collatzIter n k
+    have val_div := even_step_decrease hn heven
+    rw [val_div] at h_next_odd
+    suffices (3*(val/2)+1)/2<val by exact this
+    have : 3*(val/2)+1 ≤3*(val/2)+val/2 := by
+      have :1 ≤ val/2 := by linarith
+      linarith
+    linarith
+  · -- If next is even, (k+1) is even and smaller
+    use k+1
+    constructor; linarith
+    constructor;exact Nat.not_odd_iff_even.mp h_next_odd
+    rw [even_step_decrease hn heven]
+    exact Nat.div_lt_self (by linarith) (by norm_num)
+
+/-- From any value >1, find a smaller value -/
+theorem reach_smaller {n k : Nat} (hn : n > 0) (hgt : collatzIter n k > 1) :
+  ∃ j, j > k ∧ collatzIter n j < collatzIter n k := by
+  have val := collatzIter n k
+  by_cases heven : Even val
+  · rcases bounded_growth_between_even hn k heven with ⟨j,hj_gt,_,hj_small⟩
+    exact ⟨j,hj_gt,hj_small⟩
+  · -- If odd, then next is even:
+    have h_next_even := odd_gives_even heven.not_even_iff_odd.mp
+    rcases bounded_growth_between_even hn (k+1) h_next_even with ⟨j,hj_gt,_,hj_small⟩
+    use j
+    constructor
+    · linarith
+    · exact hj_small
+
+/-- Main theorem: Collatz conjecture -/
+theorem collatz_conjecture {n : Nat} (hn : n > 0) :
+  ∃ k, collatzIter n k = 1 := by
+  let S := {m | ∃ k, collatzIter n k = m}
+  have hne : S.Nonempty := ⟨n,0,rfl⟩
+
+  -- Extract minimal element m from S
+  obtain ⟨m,hm_in,hmin⟩ := WellFounded.min Nat.lt_wf S hne
+  rcases hm_in with ⟨K,hK⟩
+
+  -- If m=1 or we get contradiction
+  by_contra h
+  have m_pos := collatzIter_pos hn K
+  have : m > 1 := Nat.lt_of_le_of_ne m_pos (Ne.symm h)
+  rcases reach_smaller hn this with ⟨j,hj_gt,hj_small⟩
+  have : collatzIter n j ∈ S := ⟨j,rfl⟩
+  exact Nat.lt_irrefl m (lt_of_lt_of_le hj_small (hmin _ this))

Main.lean

@@ -0,0 +1,6 @@
+import Collatz
+
+def main : IO Unit := do
+  IO.println s!"Hello, {hello}!"
+  let test : Prop := ∃ k, collatzIter 5 k = 1
+  IO.println s!"Test: {test}"

lake-manifest.json

@@ -0,0 +1,95 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a608095eeb63e987177b864f008097d95c70abfe",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.15.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.15.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.48",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.14.0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "74dffd1a83cdd2969a31c9892b0517e7c6f50668",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "collatz",
+ "lakeDir": ".lake"}

lakefile.toml

@@ -0,0 +1,14 @@
+name = "collatz"
+version = "0.1.0"
+defaultTargets = ["collatz"]
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+
+[[lean_lib]]
+name = "Collatz"
+
+[[lean_exe]]
+name = "collatz"
+root = "Main"

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.15.0-rc1