diff --git a/MathTest.lean b/MathTest.lean
index 5be7cdf..c221361 100644
--- a/MathTest.lean
+++ b/MathTest.lean
@@ -1 +1,2 @@
 import MathTest.Basic
+import MathTest.Theorems
diff --git a/MathTest/Theorems.lean b/MathTest/Theorems.lean
new file mode 100644
index 0000000..c8fc2e5
--- /dev/null
+++ b/MathTest/Theorems.lean
@@ -0,0 +1,2 @@
+import MathTest.Theorems.exists_sequence_intersects_all_rational_lines
+
diff --git a/MathTest/Theorems/exists_sequence_intersects_all_rational_lines.lean b/MathTest/Theorems/exists_sequence_intersects_all_rational_lines.lean
new file mode 100644
index 0000000..4bd3ee6
--- /dev/null
+++ b/MathTest/Theorems/exists_sequence_intersects_all_rational_lines.lean
@@ -0,0 +1,18 @@
+import Mathlib
+
+namespace MathTest
+
+theorem exists_sequence_intersects_all_rational_lines :
+    ∃ s : ℕ → ℚ, ∀ a d : ℚ, ∃ t : ℕ, s t = a + d * (t : ℚ) := by
+  classical
+  let s : ℕ → ℚ := fun t =>
+    match Encodable.decode (α := ℚ × ℚ) t with
+    | some p => p.1 + p.2 * (t : ℚ)
+    | none => 0
+  refine ⟨s, ?_⟩
+  intro a d
+  refine ⟨Encodable.encode (a, d), ?_⟩
+  simp [s, Encodable.encodek (α := ℚ × ℚ) (a, d)]
+
+end MathTest
+