Demostrar con Lean4 que existen infinitos n\u00fameros primos.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Tactic\r\nimport Mathlib.Data.Nat.Prime\r\nopen Nat\r\n\r\nexample\r\n (n : \u2115) :\r\n \u2203 p, n \u2264 p \u2227 Nat.Prime p :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Se usar\u00e1n los siguientes lemas de los n\u00fameros naturales, donde \\(\\text{Primo}(n)\\) se verifica si \\(n\\) es primo y \\(\\text{minFac}(n)\\) es el menor factor primo de \\(n\\).<\/p>\n
\\begin{align}
\n &n \u2260 1 \u2192 \\text{Primo}(\\text{minFac}(n)) \\tag{L1} \\\\
\n &n! > 0 \\tag{L2} \\\\
\n &0 < k \u2192 n < k + n \\tag{L3} \\\\\n &k < n \u2192 n \u2260 k \\tag{L4} \\\\\n &k \u2271 n \u2192 k \u2264 n \\tag{L5} \\\\\n &0 < k \u2192 k \u2264 n \u2192 k \u2223 n! \\tag{L6} \\\\\n &0 < \\text{minFac}(n) \\tag{L7} \\\\\n &k \u2223 m \u2192 (k \u2223 n \u2194 k \u2223 m + n) \\tag{L8} \\\\\n &\\text{minFac}(n) \u2223 n \\tag{L9} \\\\\n &\\text{Primo}(n) \u2192 \u00acn \u2223 1 \\tag{L10}\n\\end{align}\n\nSea \\(p\\) el menor factor primo de \\(n! + 1\\). Tenemos que demostrar que \\(n \u2264 p\\) y que \\(p\\) es primo.\n\nPara demostrar que \\(p\\) es primo, por el lema L1, basta demostrar que\n\\[ n! + 1 \u2260 1 \\]\nSu demostraci\u00f3n es\n\\begin{align}\n &n ! > 0 &&\\text{[por L2]} \\\\
\n &\u27f9 n ! + 1 > 1 &&\\text{[por L3]} \\\\
\n &\u27f9 n ! + 1 \u2260 1 &&\\text{[por L4]}
\n\\end{align}<\/p>\n
Para demostrar \\(n \u2264 p\\), por el lema L5, basta demostrar que \\(n \u2271 p\\). Su demostraci\u00f3n es
\n\\begin{align}
\n &n \u2265 p \\\\
\n &\u27f9 p \u2223 n! &&\\text{[por L6 y L7]} \\\\
\n &\u27f9 p | 1 &&\\text{[por L8 y \\(p | n! + 1\\) por L9]} \\\\
\n &\u27f9 \\text{Falso} &&\\text{[por L10 y \\(p\\) es primo]}
\n\\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\r\nimport Mathlib.Tactic\r\nimport Mathlib.Data.Nat.Prime\r\nopen Nat\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (n : \u2115) :\r\n \u2203 p, n \u2264 p \u2227 Nat.Prime p :=\r\nby\r\n let p := minFac (n ! + 1)\r\n have h1 : Nat.Prime p := by\r\n apply minFac_prime\r\n -- \u22a2 n ! + 1 \u2260 1\r\n have h3 : n ! > 0 := factorial_pos n\r\n have h4 : n ! + 1 > 1 := Nat.lt_add_of_pos_left h3\r\n show n ! + 1 \u2260 1\r\n exact Nat.ne_of_gt h4\r\n use p\r\n constructor\r\n . -- \u22a2 n \u2264 p\r\n apply le_of_not_ge\r\n -- \u22a2 \u00acn \u2265 p\r\n intro h5\r\n -- h5 : n \u2265 p\r\n -- \u22a2 False\r\n have h6 : p \u2223 n ! := dvd_factorial (minFac_pos _) h5\r\n have h7 : p \u2223 1 := (Nat.dvd_add_iff_right h6).mpr (minFac_dvd _)\r\n show False\r\n exact (Nat.Prime.not_dvd_one h1) h7\r\n . -- \u22a2 Nat.Prime p\r\n exact h1\r\n done\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (n : \u2115) :\r\n \u2203 p, n \u2264 p \u2227 Nat.Prime p :=\r\nexists_infinite_primes n\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- variable (k m n : \u2115)\r\n-- #check (Nat.Prime.not_dvd_one : Nat.Prime n \u2192 \u00acn \u2223 1)\r\n-- #check (Nat.dvd_add_iff_right : k \u2223 m \u2192 (k \u2223 n \u2194 k \u2223 m + n))\r\n-- #check (Nat.dvd_one : n \u2223 1 \u2194 n = 1)\r\n-- #check (Nat.lt_add_of_pos_left : 0 < k \u2192 n < k + n)\r\n-- #check (Nat.ne_of_gt : k < n \u2192 n \u2260 k)\r\n-- #check (dvd_factorial : 0 < k \u2192 k \u2264 n \u2192 k \u2223 n !)\r\n-- #check (factorial_pos n: n ! > 0)\r\n-- #check (le_of_not_ge : \u00ack \u2265 n \u2192 k \u2264 n)\r\n-- #check (minFac_dvd n : minFac n \u2223 n)\r\n-- #check (minFac_pos n : 0 < minFac n)\r\n-- #check (minFac_prime : n \u2260 1 \u2192 Nat.Prime (minFac n))\r\n<\/pre>\nDemostraciones interactivas<\/h3>\n