On 2 September 2026 New York City Public Schools restricted student-facing generative AI — the policy names chatbots and AI tutors — for grades 2-K through 8, and capped individual screen time at 30 minutes in grades 3–5 and 45 minutes in middle school. Teachers keep approved AI for lesson planning, translation and drafting communications; they lose it for grading, behaviour monitoring and counselling.
Read it closely. It does not say no computers. It does not say no mathematics done with machines. It names one category of tool: the kind that produces an answer a child has no way to check.
A proof assistant is the opposite machine. It produces nothing. It reads what the child wrote, and returns one of two things: silence, or a red underline. It cannot be flattered, it cannot be prompted into agreeing, and it has no view about whether the child is doing well. Every activity in this course runs on that machine, and there is no chatbot in the room.
The course is written for after-school hours, where the Department’s screen caps do not formally reach. It observes them anyway: 45 minutes on the machine, 30 off. The half off the machine is where the thinking happens.
Not a certificate. A ledger — one page, about a file they wrote themselves, carrying three numbers:
The first two are ordinary schoolwork in an unfamiliar costume. The third is not taught anywhere, at any level, and it is at this moment the thing professional mathematicians are arguing about. A child who has run one command on their own theorem and written down what it said has done something a good many published results have not. That claim is made precisely, with the evidence, at the end of this page.
| Machine | Any browser, at live.lean-lang.org. Nothing is installed and nothing is signed into. If the school lends the laptop, nothing on this course asks the school for permission to install software. |
|---|---|
| Pairs | One machine per two children beats one each. The argument between the pair is most of the learning; a child alone with a checker just guesses faster. |
| Paper | Every child keeps one notebook for all eight weeks. Numbers written in it are never erased, only crossed out and rewritten with the date. This is a habit, not a rule about tidiness. |
| The grown-up | Does not need to know Lean. You need to be able to read an error message out loud and ask the room what it is telling us. |
Each child writes down three statements about numbers: one they are certain is true, one they are certain is false, and one they are not sure about. The third one is collected and kept. It comes back in session 8, and telling them that now is part of the design.
Open the editor. Type this and wait.
theorem easy : 2 + 2 = 4 := by decideNothing happens. Say plainly what just happened: this machine says yes by saying nothing. There is no praise, no green tick, no encouragement. Silence is the whole of its approval, and children find this much more interesting than adults expect.
Now break it on purpose.
theorem wrong : 2 + 2 = 5 := by decideCopy the error into the notebook word for word. Then break it a second, different way:
theorem alsowrong : 2 + 2 = 4 := by rfl2A different error. Two kinds of no, and the distinction is the session: what you said is false is not the same as I do not understand what you asked me. Children who never separate these two spend the rest of the course thinking the machine dislikes them.
They will type enormous numbers to see what happens. Let them — and when the editor stalls or gives up, you have been handed the third kind of no for free: I cannot finish. Three kinds of no, day one, written in the notebook.
Invent a game together — a board game, a playground game, anything with rules. Write the rules on the board. Then ask the room: which of these did we prove, and which did we simply decide? Every game rests on things nobody argued for. So does mathematics, and there they are called axioms.
Go back to last week’s theorem and ask the machine what it stood on.
#print axioms easyRead the answer out loud. Write it in the notebook exactly as it appears. Then give the three names their one sentence each:
| propext | Two statements that are true in exactly the same situations count as the same statement. |
|---|---|
| Quot.sound | If you decide to treat two things as the same thing, then they are the same thing. |
| Classical.choice | Every question has an answer, even when nobody can point to it. |
The third is the session. Ask them whether they believe it. Some mathematicians do not, and have built a whole mathematics without it. A room of eleven-year-olds will split roughly down the middle, and they will be splitting along a real fault line, not a pretend one.
Someone asks who decided there were three. This is the best question of the course. The answer: the people who built this particular checker. A different checker has a different list, written in a different format, and comparing the two is genuinely difficult — which is why grown-ups are currently paid to work on it.
sorryType a claim nobody in the room can prove, and hand it to the machine unfinished.
theorem doubling (n : Nat) : n < 2 ^ n := by
sorryIt is accepted. And it is marked — a warning appears saying the declaration uses sorry. Read it aloud.
State the rule of the course, and mean it: you are allowed to claim anything you have not proved, as long as the claim carries the mark. What you are never allowed to do is remove the mark.
sorry is notsorry has said, in public and in permanent ink, exactly where their work stops — which is more than most people manage.
Everyone writes down one thing they believe but cannot prove — about numbers, about the world, about their sister — and writes sorry beside it. These go on the wall and stay there all eight weeks. Some of them will come down before session 8. Most will not, and that is the honest ratio.
The strongest session. It works every time.
Hand out counting.lean (below, or from the folder beside this page). It is a file with eight claims in it. Ask a single question: how many sorries are in this file?
Three numbers, one file, none of them wrong. Then the question that is the reason this course exists: which one do you report?
Answer: whichever you like — provided you say how you counted. A number quoted without its method cannot be compared to anybody else’s number. That sentence goes in every notebook.
Each pair writes a one-sentence counting rule good enough that another pair, given the same file, gets the same number. Swap and test. They will not agree on the first try; the negotiation is the lesson.
theorem n_plus_n_is_even (n : Nat) : (n + n) % 2 = 0 := by
omegaSilence. It holds — for every number there is, all at once, including the ones nobody has ever written down.
Now take the tactic away and put decide in its place. It fails, and the failure is the point: decide works something out for a particular number, and here there is no particular number. There is n.
Ask: how many numbers would you have to check by hand to be sure of this? They will start counting and then stop counting. That stop is the difference between testing a thing and proving it, and they now have it in their hands rather than in a definition.
A child will want to know what omega is doing. You do not have to know. “It is a proof-finder for arithmetic, and next week we will make it show us what it used” is a true and sufficient answer, and it sets up session 6.
The same claim, twice, by two routes — then ask the machine what each route cost.
theorem even_a (n : Nat) : (n + n) % 2 = 0 := by
omega
theorem even_b (n : Nat) : (n + n) % 2 = 0 := by
induction n with
| zero => decide
| succ k ih => omega
#print axioms even_a
#print axioms even_bSomeone will try to build a proof deliberately expensive enough to make the lists differ. Let them, and give them the rest of the session. That is not a distraction from the curriculum. That is the curriculum, arriving early.
Each pair writes one file of their own containing at least five claims. Some proved, some carrying sorry. It is theirs; it does not have to be impressive, and a file of five true easy things is a better artifact than a file of one ambitious wreck.
Then the page they take home:
sorry The last line is not decoration and it is not optional. It is the line that makes the four numbers above it mean anything at all, and a ledger handed in without it goes back.
Each pair presents their ledger, and the room has exactly one job: attack the numbers, never the mathematics. Permitted questions are “how did you count that?”, “does the machine agree?”, and “show us the warning”. Not permitted: “that proof is easy”. Easy is fine. Unaccounted-for is not.
Hand back the third statement from session 1 — the one they were not sure about, seven weeks ago, before any of this. Ask them to write it in Lean. Not to prove it. To state it, precisely enough that a machine could tell them whether it holds.
Most of them will manage it. A few will discover their statement was never quite a statement, which is the more valuable outcome and should be said so out loud. That is the course.
counting.lean-- Zero Sorries · Session 4 · counting.lean
-- Count the word "sorry" in this file. Write your number down.
-- Then count it again a different way. Then a third way.
-- Claim 1. Adding a number to itself gives an even number.
theorem claim1 (n : Nat) : (n + n) % 2 = 0 := by
omega
-- Claim 2. Every number is smaller than two raised to that number.
-- We have not proved this one, so it gets a sorry.
theorem claim2 (n : Nat) : n < 2 ^ n := by
sorry
-- Claim 3. Four is not five.
theorem claim3 : 4 ≠ 5 := by
decide
/- Claim 4. Two odd numbers added together give an even number.
Someone proved this on paper last week but nobody typed it in,
so for now it is a sorry. -/
theorem claim4 (a b : Nat) (ha : a % 2 = 1) (hb : b % 2 = 1) :
(a + b) % 2 = 0 := by
sorry
-- Claim 5. Zero is less than one.
theorem claim5 : 0 < 1 := by
decide
/- Claim 6. Doubling a number and then halving it gives back the number.
This is the one that took three tries. The first two attempts are in
the notebook; a sorry holds the place until one of them works. -/
theorem claim6 (n : Nat) : (2 * n) / 2 = n := by
sorry
-- Claim 7. A number plus zero is that number.
theorem claim7 (n : Nat) : n + 0 = n := by
rfl
-- Claim 8. Every even number bigger than two is the sum of two primes.
-- Nobody has proved this. Not us, not anyone, since 1742.
-- No sorry will help here: we cannot even write the claim down yet.
-- That is session 8.By eye, seven. By find, eight. By the machine, three. Claim 6 is deliberately provable and deliberately left unproved — if a child notices and fixes it, the ledger changes and they have understood the whole thing.
No child in this course uses generative AI, and the course is nonetheless aimed at the centre of what is currently called AI for mathematics. Here is the argument, without softening.
Machines are now producing real mathematics. In a single eight-day stretch this September, three separate groups published formal results: a bound on gaps between primes, a second and different bound on gaps between primes, and a machine-checked formalization of Fermat’s Last Theorem. All three rested on material outside the proofs they published. All three described that fact differently — one called them hypotheses taken, one wrote them as explicit assumption declarations, one made an assumption check the definition of a passing build. A reader could not say which of them assumed more.
The command that answers the question is #print axioms. It has existed the whole time. What does not exist is the habit of running it and reporting the answer in a form somebody else can compare.
A habit that does not exist among professionals has to be taught to somebody. It is a school subject, and it needs no chatbot, no model, no account, and no permission slip. A twelve-year-old who has run #print axioms on a theorem they wrote themselves, and written the answer on a piece of paper, and then defended that piece of paper against a room, has practised the thing the field is short of.
That is the whole claim of this course, and it does not require believing anything optimistic about children or about machines.
Eight weeks, one afternoon a week, 75 minutes. Grades 5–8. Free. Nothing to install, nothing to sign up for, no equipment beyond a borrowed laptop and a notebook.
Is this the AI the schools just restricted? No. The city’s September 2026 policy restricts chatbots and AI tutors for grades 2-K through 8 — tools that write things for a child. This course uses a proof checker, which writes nothing. Your child types a mathematical statement; the machine reports whether it holds. It gives no answers, offers no suggestions, and cannot be asked to do the work. There is no chatbot in the room and no child talks to a model.
What do they come home with? A one-page ledger about a file of mathematics they wrote themselves: what they claimed, what they proved, what they had to assume, and — the line that matters — how they counted. Ask them that last one. They will have an answer, and they will be able to defend it.
What does it need from me? That the notebook survives eight weeks, and that nobody erases a number in it.
Run by a parent, not by the school. Materials are open and free to copy: any adult who can read an error message aloud can run this room.