lean_workbook_plus_59983

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

It is not needed. The goo gets longer by a factor of $1.6 \times 1.25=2$ every day, so it is just asking the smallest power of 2 that is larger than 2017. The power of 2 is $2^{11}=2048$ , so that will happen at 11 days after the beginniing Monday, which is a Thursday.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59983  (n : ℕ)
  (h₀ : 0 < n)
  (h₁ : 2^n > 2017) :
  11 ≤ n   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph