Prove It with Lean

Baccare Labs · a reasoning track for grades 5 and 6

Prove It with Lean

Lean is a program that checks mathematical proofs. Universities and research labs use it to make sure long, difficult arguments have no gaps. We use a tiny slice of it to teach something every 10- and 11-year-old is ready for: the difference between "I checked some examples" and "I showed it must be true."

For parents, in one paragraph. Your child will not become a programmer from this track, and that is not the goal. They will learn to read a short statement, recognize what is being claimed, and pick the step that justifies it, with a computer that refuses to accept a gap. Everything is done inside Baccare's activities. No installation, no accounts, no typing Lean code. The optional playground at the end is for curious parents and kids who want to try the real thing together.

Baccare Labs, not curriculum. Lean is not part of the Texas Essential Knowledge and Skills and no Texas standard requires it. This track is part of Baccare Labs: it exercises the reasoning and justification skills the math standards ask for, using a tool the standards do not mention. Check-ups and progress reports keep it separate from required work.

Why introduce a proof checker at this age

Texas math standards ask 5th and 6th graders to "justify the solution," "analyze mathematical relationships," and "display, explain, and justify mathematical ideas and arguments using precise mathematical language." Those are the process standards that run through every grade, and they are the hardest to practice on a worksheet. A proof checker gives immediate, impartial feedback on exactly that skill: was the step you chose actually justified? Lean also happens to be the tool that the world's mathematicians are now using to verify research, so a child who meets it at 10 meets it again in college with a head start.

We keep the scope small on purpose. At this level a proof is three or four moves long, every number is a whole number, and the proofs are about facts the child already believes (2 + 3 = 5, adding zero changes nothing, n + 1 is bigger than n). The new idea is not the math. The new idea is that "obviously true" has to be earned.

What is on the track

5th grade · Meet LeanWhat a proof is. Reading a goal. The word by. Your first tactic, rfl: "both sides are the same thing." Why Lean says "goals accomplished," and why it refuses 2 + 2 = 5.Play the activity →

5th grade · TacticsNaming a fact with theorem. Hypotheses. rw [h]: rewrite the goal using something you know. decide: let Lean settle a yes-or-no question. What (n : Nat) means, and why one proof can cover every number.Play the activity →

6th grade · Every numberThe ∀ symbol. intro, exact, and omega. The domino idea behind induction: prove it for 0, prove each number passes it to the next, and infinitely many cases fall at once. Why 0 + n = n is harder than n + 0 = n.Play the activity →

How to do this at the kitchen table

Start with a skeptic game, no screen. Say "3 + 4 = 7." Ask your child to convince you without a calculator. Then be difficult: "How do you know?" Every answer they give, ask again. That feeling, running out of "because," is exactly what a proof fixes.
Play "Meet Lean" together the first time. Read each Lean line aloud. The colon means "here is what I claim." The := means "and here is the proof." The word after by is the move.
Let them name the move before tapping. "Both sides are the same after computing" is rfl. "Swap in something I know" is rw. "Just check it" is decide. Three moves, three sentences.
Celebrate a rejected proof. When Lean refuses 2 + 2 = 5, that is the whole lesson: the checker is not on anyone's side. It is on the side of what is true.
Ask Bacc if they get stuck. Bacc knows this track and will give a hint about which move fits, never the answer.

Vocabulary, kid-sized

Goal: the thing you are trying to prove. It sits between the colon and :=.
Tactic: a move that changes or finishes a goal. rfl, rw, decide, intro, exact, omega.
Hypothesis: a fact you are allowed to use, with a name like h.
Theorem: a proved fact with a name, saved so later proofs can use it.
Nat: the natural numbers 0, 1, 2, 3, … forever. (n : Nat) means "n is any one of them."
Induction: the domino method. Prove it for 0; prove each number passes it to the next.

Optional: try real Lean, together

Lean has a free browser playground at live.lean-lang.org. It needs no account. Paste this and watch the right-hand panel:

example : 2 + 3 = 5 := by
  rfl

example : 2 + 3 = 6 := by
  rfl   -- Lean will complain here. Ask your child why.

theorem add_zero_right (n : Nat) : n + 0 = n := by
  rfl

This is an outside website run by the Lean community, not by Baccare. It is appropriate for children with a parent alongside, but we do not control it, and it is a full programming tool with far more in it than this track covers. The Natural Number Game, also free and browser-based, is the natural next step for a 6th grader who wants more; it turns induction into a level-by-level puzzle.

Where this goes

The track stops at induction on purpose. Middle-school algebra is where variables, equations, and "for every x" become daily work, and a student who has already met a proof checker arrives knowing that an equation is a claim, not a command. We will add levels as the 6th-grade standards are fully mapped and as families tell us what worked.

Start with Meet Lean 5th grade math course