25 enero 2024 – Calculemus

Existen infinitos números primos

PorJosé A. Alonso 25 enero 202424 enero 2024

Demostrar con Lean4 que existen infinitos números primos.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
import Mathlib.Data.Nat.Prime
open Nat

example
  (n : ℕ) :
  ∃ p, n ≤ p ∧ Nat.Prime p :=
by sorry

import Mathlib.Tactic

import Mathlib.Data.Nat.Prime

open Nat

example

(n : ℕ) :

∃ p, n ≤ p ∧ Nat.Prime p :=

by sorry