Practice: First steps in Lean

First steps in Lean

Warm-upFormal

Let n : ℕ be a variable. Which of these goals can be closed by rfl alone? (Choose all that apply.)

Choose all that apply

n + 0 = n2 + 3 = 50 + n = nn + 1 = 1 + n

First steps in Lean

Warm-upFormal

A classmate's Lean file compiles with the warning "declaration uses sorry". What can you conclude?

Choose one

The theorem is not proved: sorry is a placeholder Lean accepts on trust, and #print axioms would list sorryAx.The theorem is proved, because the file compiles.The theorem is false.Lean found a proof automatically and is warning that it is long.

First steps in Lean

Warm-upFormal

In Lean, what is the value of (7 : ℕ) - 10?

First steps in Lean

Warm-upFormal

In Lean, what is the value of (17 : ℕ) / 5?

First steps in Lean

CoreFormal

You are proving theorem t (p q : Prop) : p → (q → p) := by and you type intro hp. What does the goal state look like now?

Choose one

Hypotheses p q : Prop and hp : p; goal ⊢ q → pHypotheses p q : Prop and hp : p → q; goal ⊢ pHypotheses p q : Prop; goal ⊢ pNo goals: the proof is complete.

First steps in Lean

CoreFormal

Which term is a proof of p ∧ q → q ∧ p?

Choose one

fun ⟨hp, hq⟩ => ⟨hq, hp⟩fun ⟨hp, hq⟩ => ⟨hp, hq⟩fun h => h⟨hq, hp⟩

First steps in Lean

CoreFormal

The theorem no_nat_sqrt_two : ¬ ∃ q : ℕ, q * q = 2 is proved in Lean without sorry. Does it show that $\sqrt 2$ is irrational?

Choose one

No. It only says no natural number squares to

2

; irrationality is about fractions, which this statement never mentions.Yes, because Lean checked it.Yes, because every rational number is a natural number.No, because the proof must be wrong.

First steps in Lean

CoreFormal

Mathlib contains theorem Nat.exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p. Which reading is correct?

Choose one

For every natural number

n

there is a prime

p

with

p \ge n

.There is a prime

p

that is at least as big as every natural number

n

.Every natural number

p \ge n

is prime.There are exactly

n

primes.

First steps in Lean

StretchFormal

In the induction proof of 0 + n = n, the inductive step has hypothesis ih : 0 + k = k and goal ⊢ 0 + (k + 1) = k + 1. Which tactic line closes the goal?

Choose one

rw [Nat.add_succ, ih]rw [ih]rflexact ih

First steps in Lean

CoreComputational

Truth tables decide propositional tautologies by brute force. Write is_tautology(formula, n), where formula is a Python function of n Booleans, returning True exactly when it is true for all $2^n$ assignments. (In Python, p <= q on Booleans means $p \to q$ .)

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.