funlean.
Step 1 / 64

High school

Reading a Lean statement

Separate the objects, their conditions, and the conclusion.

Start with a concrete example

“Choose a positive whole number” does not allow 0 or a negative number. Move n and check whether n > 0 is true. A condition is something to check, not part of a name.

n > 0This number satisfies the condition

n = 1：1 > 0 ✓

How this example differs from the definition

This checks one numerical condition, not a Lean proof or all the hypotheses of the chapter.

A small check: try the idea

Compare the numbers in the question with the diagram you are moving. You can try again.

Does n=0 satisfy the condition n>0?

Read the answer and reasoning

No. 0 is a whole number, but it is not positive. The object and the extra condition are separate checks.

Build the idea in three steps

  1. Start with the objects: (a : ℕ) means a is a natural number. ℕ includes zero; ℤ also includes negative integers.
  2. A condition is itself a statement. ha : 0 < a names evidence that a is positive. Prop is the type of statements.
  3. Read ∀ as “for every”, ∃ as “there exists”, ∧ as “and”, and → as “if … then …”. A structure bundles objects with evidence for its fields.

A small example

In the package, a : ℤ is a number, while ha0 : a ≠ 0 is evidence about that number.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_FreyPackage.lean

structure FreyPackage where   a : ℤ   b : ℤ   c : ℤ  ha0 : a ≠ 0  hb0 : b ≠ 0  hc0 : c ≠ 0   p : ℕ  pp : Nat.Prime p  hp5 : 5 ≤ p   hFLT : a ^ p + b ^ p = c ^ p   hgcdab : gcd a b = 1   ha4 : (a : ZMod 4) = 3

How to read this Lean

Read the data fields a, b, c first; then their ha0, hb0, hc0 evidence. A field name is not a new mathematical concept.

Original source ↗ · L17–37Open the complete saved source

Where this idea is used

1. The impossible order2. The case of three3. Too many suspects4. The suitcase diet5. The suspicious parcel6. The scissors incident7. The veterans’ cabinet8. The secret duet9. Two doors to the concert10. A three-note audition11. Borrow a better passport12. The workshops agree13. Pip’s impossible quilt14. The shrinking reservation15. The concert of absolute silence16. The room with no room17. The extremely literal judge
I’m lost · Help

Mika’s help desk

Reading a Lean statement

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

Separate the objects, their conditions, and the conclusion.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

In the package, a : ℤ is a number, while ha0 : a ≠ 0 is evidence about that number.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →