Skip to main content

Posts about Lean4Challenge (old posts, page 2)

RSS feed (Lean4Challenge, en)

Canal RSS (RetoLean4, es)

Also available in:

Español (RetoLean4)

Challenge 6: If aₙ and cₙ converge to L and aₙ ≤ bₙ ≤ cₙ for all n, then bₙ converges to L

Lean 4 Challenges/Analysis/Limits

Prove the squeeze theorem; that is, if \(a_n\) and \(c_n\) converge to \(L\) and \(a_n ≤ b_n \leq c_n\) for all \(n\), then \(b_n\) converges to \(L\).

To do so, complete the following Lean 4 theory:

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

variable {a b c : ℕ → ℝ}
variable {L : ℝ}

def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

example
  (ha : SeqLim a L)
  (hc : SeqLim c L)
  (hab : ∀ n, a n ≤ b n)
  (hbc : ∀ n, b n ≤ c n)
  : SeqLim b L := by
  sorry

Read more…

Challenge 5: 5²ⁿ - 2³ⁿ is divisible by 17

Lean 4 Challenges/Number theory/Induction

Prove in Lean 4 that 5²ⁿ - 2³ⁿ is divisible by 17 for every natural number n.

To do so, complete the following Lean 4 theory:

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

variable (n : ℕ)

open Nat

example : 17 ∣ 5^(2 * n) - 2^(3 * n) := by
  sorry

Read more…

Challenge 3: If aₙ converges to L, then 2aₙ converges to 2L

Lean 4 Challenges/Analysis/Limits

Prove in Lean 4 that if the sequence \(aₙ\) converges to \(L\), then \(2aₙ\) converges to \(2L\).

To do so, complete the following Lean 4 theory:

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

variable {a : ℕ → ℝ}

def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

example
  (ha : SeqLim a L)
  (hb : ∀ n, b n = 2 * a n)
  : SeqLim b (2 * L) :=
by
  sorry

Read more…

Challenge 2: The sequence 1, -1, 1, -1,... is not convergent

Lean 4 Challenges/Analysis/Limits

Prove that the sequence defined by 1, -1, 1, -1, ... does not converge.

To do so, the following proof in Lean 4 is to be completed:

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

variable {a : ℕ → ℝ}

def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

example
  (ha : ∀ n, a n = (-1) ^ n)
  : ¬ SeqConv a :=
by sorry

Read more…

Challenge 1: The sequence 1/n converges to 0

Lean 4 Challenges/Analysis/Limits

In Lean, a sequence \(a₀, a₁, a₂,...\) can be represented by a function \(a : ℕ → ℝ\) so that \(a(n)\) is \(aₙ\).

The statement that \(L\) is the limit of the sequence \(a\) is defined by

def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

Prove that if \(aₙ = 1/n\) for all \(n\), then the sequence \(a\) converges to 0.

To do so, complete the following Lean 4 theory:

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

variable (a : ℕ → ℝ)

def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

example
  (ha : ∀ n, a n = 1 / n)
  : SeqLim a 0 :=
by sorry

Read more…

Proof challenges in Lean 4

Lean 4 Challenges

I have started publishing the series Mathematical challenges in Lean 4.

The format is simple: each week I will post a mathematical problem so that anyone interested can share their solutions in Lean 4.

At the end of the week I will publish the solutions to the challenge, which will follow this scheme:

  1. A solution in natural language.
  2. Several Lean 4 formalizations, from least to most detailed:
    1. The most automated one, usually with grind.
    2. Others using more specific tactics, such as norm_num, ring, positivity or linarith.
    3. A final proof in which those tactics are replaced by specific lemmas.

Through this process of successive refinement, the aim is for the final proof to correspond, as far as possible, to the one written in natural language.