Skip to main content

Posts about Number theory

Subcategories:

RSS feed (Number theory, en)

Nicomachus’s theorem

Number theory/Induction

Prove the Nicomachus's theorem which states that the sum of the cubes of the first \(n\) natural numbers is equal to the square of the sum of the first \(n\) natural numbers; that is, for any natural number n we have \[ 1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2 \]

To do this, complete the following Lean4 theory:

import Mathlib.Data.Nat.Defs
import Mathlib.Tactic

open Nat

variable ( n : ℕ)

def sum : ℕ → ℕ
  | 0      => 0
  | succ n => sum n + (n+1)

def sumCubes : ℕ → ℕ
  | 0   => 0
  | n+1 => sumCubes n + (n+1)^3

example :
  sumCubes n = (sum n)^2 :=
by sorry

Read more…

Proofs of "If p > -1, then (1+p)ⁿ ≥ 1+np"

Number theory/Induction

Let \(p ∈ ℝ\) and \(n ∈ ℕ\). Prove that if \(p > -1\), then \[ (1 + p)^n ≥ 1 + np \]

To do this, complete the following Lean4 theory:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

open Nat

variable (p : ℝ)
variable (n : ℕ)

example
  (h : p > -1)
  : (1 + p)^n ≥ 1 + n*p :=
by sorry

Read more…

Proofs of 0³+1³+2³+3³+···+n³ = (n(n+1)/2)²

Number theory/Induction

Prove that the sum of the first cubes \[ 0^3 + 1^3 + 2^3 + 3^3 + ··· + n^3 \] is \[ \dfrac{n(n+1)}{2}^2 \]

To do this, complete the following Lean4 theory:

import Mathlib.Data.Nat.Defs
import Mathlib.Tactic

open Nat

variable (n : ℕ)

def sumCubes : ℕ → ℕ
  | 0   => 0
  | n+1 => sumCubes n + (n+1)^3

example :
  4 * sumCubes n = (n*(n+1))^2 :=
by sorry

Read more…

Proofs of a+aq+aq²+···+aqⁿ = a(1-qⁿ⁺¹)/(1-q)

Number theory/Induction

Prove that if \(q ≠ 1\), then the sum of the terms of the geometric progression \[ a + aq + aq^2 + ··· + aq^n \] is \[ \dfrac{a(1 - q^{n+1})}{1 - q} \]

To do this, complete the following Lean4 theory:

import Mathlib.Data.Nat.Defs
import Mathlib.Tactic

open Nat

variable (n : ℕ)
variable (a q : ℝ)

def sumGP : ℝ → ℝ → ℕ → ℝ
  | a, _, 0     => a
  | a, q, n + 1 => sumGP a q n + (a * q^(n + 1))

example
  (h : q ≠ 1)
  : sumGP a q n = a * (1 - q^(n + 1)) / (1 - q) :=
by sorry

Read more…

Proofs of a+(a+d)+(a+2d)+···+(a+nd)=(n+1)(2a+nd)/2

Number theory/Induction

Prove that the sum of the terms of the arithmetic progression \[ a + (a + d) + (a + 2d) + ··· + (a + nd) \] is \[ \dfrac{(n + 1)(2a + nd)}{2} \]

To do this, complete the following Lean4 theory:

import Mathlib.Data.Nat.Defs
import Mathlib.Tactic

open Nat

variable (n : ℕ)
variable (a d : ℝ)

def sumAP : ℝ → ℝ → ℕ → ℝ
  | a, _, 0     => a
  | a, d, n + 1 => sumAP a d n + (a + (n + 1) * d)

example :
  2 * sumAP a d n = (n + 1) * (2 * a + n * d) :=
by sorry

Read more…

Proofs of "0+1+2+3+···+n=n(n + 1)/2"

Number theory/Induction

Prove that the sum of the natural numbers \[ 0 + 1 + 2 + 3 + ··· + n \] is \[\dfrac{n(n + 1)}{2}\]

To do this, complete the following Lean4 theory:

import Init.Data.Nat.Basic
import Mathlib.Tactic

open Nat

variable (n : Nat)

set_option pp.fieldNotation false

def sum : Nat → Nat
  | 0      => 0
  | succ n => sum n + (n+1)

example :
  2 * sum n = n * (n + 1) :=
by sorry

Read more…

If (∀ ε > 0, y ≤ x + ε), then y ≤ x

Number theory/Real numbers

Let \(x, y ∈ ℝ\). Prove that \[ (∀ ε > 0, y ≤ x + ε) → y ≤ x \]

To do this, complete the following Lean4 theory:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {x y : ℝ}

example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
by sorry

Read more…

If x is the supremum of set A, then ((∀ y)[y < x → (∃ a ∈ A)[y < a]]

Number theory/Real numbers

In Lean4, one can define that \(x\) is an upper bound of \(A\) by

   def is_upper_bound (A : Set ℝ) (x : ℝ) :=
     ∀ a ∈ A, a ≤ x

and \(x\) is supremum of \(A\) by

   def is_supremum (A : Set ℝ) (x : ℝ) :=
     is_upper_bound A x ∧ ∀ y, is_upper_bound A y → x ≤ y

Prove that if \(x\) is the supremum of \(A\), then \[ (∀ y)[y < x → (∃ a ∈ A)[y < a]] \]

To do this, complete the following Lean4 theory:

import Mathlib.Data.Real.Basic
variable {A : Set ℝ}
variable {x : ℝ}

def is_upper_bound (A : Set ℝ) (x : ℝ) :=
  ∀ a ∈ A, a ≤ x

def is_supremum (A : Set ℝ) (x : ℝ) :=
  is_upper_bound A x ∧ ∀ y, is_upper_bound A y → x ≤ y

example
  (hx : is_supremum A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
by sorry

Read more…

Equivalence of definitions of the Fibonacci function

Number theory/Induction

In Lean4, the Fibonacci function can be defined as

   def fibonacci : Nat → Nat
     | 0     => 0
     | 1     => 1
     | n + 2 => fibonacci n + fibonacci (n+1)

Another more efficient definition is

   def fib (n : Nat) : Nat :=
     (loop n).1
   where
     loop : Nat → Nat × Nat
       | 0   => (0, 1)
       | n + 1 =>
         let p := loop n
         (p.2, p.1 + p.2)

Prove that both definitions are equivalent; that is,

   fibonacci = fib

To do this, complete the following Lean4 theory:

open Nat

set_option pp.fieldNotation false

def fibonacci : Nat → Nat
  | 0     => 0
  | 1     => 1
  | n + 2 => fibonacci n + fibonacci (n+1)

def fib (n : Nat) : Nat :=
  (loop n).1
where
  loop : Nat → Nat × Nat
    | 0   => (0, 1)
    | n + 1 =>
      let p := loop n
      (p.2, p.1 + p.2)

example : fibonacci = fib :=
by sorry

Read more…