31. Powers of two grow fast

MediumProofAcademy Pass20 points

Prove that n < 2 ^ n for every natural number n.

omega does not know how ^ behaves, but it can treat 2 ^ k as an unknown number and reason linearly about it.

Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.

Solution.lean

1theorem solution (n : Nat) : n < 2 ^ n := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

n:Nat

⊢n < 2 ^ n

ReadyLn 1, Col 1Lean 4

Draft saved in this browser