Proof Assistant Lean Kids Can Try: Math Becomes Code

A proof assistant Lean kids can actually open exists, it is free, and it runs in a browser. The Natural Number Game asks you to prove that 2 + 2 = 4, starting from almost nothing, and refuses to let you skip a step. Most teenagers find it infuriating for about twenty minutes and then cannot stop.

That experience is worth more right now than it was five years ago. When AI systems produce hundred-page proofs that are correct about half the time, understanding what mechanical verification actually does stops being a niche interest and becomes a way to think.

Key Takeaways

• Lean is an interactive theorem prover: you write a proof in a formal language and the software rejects any step that does not follow from what came before.
• The Natural Number Game (NNG4) is free, open source under Apache 2.0, runs in a browser at adam.math.hhu.de, and starts from the Peano axioms.
• The Liquid Tensor Experiment proved formalization works at research level: Peter Scholze’s December 2020 challenge was completed in Lean by July 14, 2022.
• Formalizing takes longer than writing an informal proof, which is why AI-generated proofs are piling up faster than anyone can verify them.
• The transferable skill is distinguishing “this argument convinced me” from “every step of this argument is valid.”

What a proof assistant Lean kids can use actually does

A proof assistant is software that checks mathematical arguments mechanically. You state a theorem in the system’s formal language, then supply the proof as a sequence of moves, and at each step the software knows exactly what you have established and what you still need. If you try to assert something that does not follow, it will not accept it.

Lean, currently in its fourth major version, is the one that has caught on with working mathematicians. The Lean game server is one entry point; the deeper reason Lean caught on is Mathlib, a community-built library containing a large fraction of undergraduate and graduate mathematics already formalized, so you can build on existing results instead of starting from axioms every time.

The critical distinction, and the one worth teaching, is between convincing and valid. A human proof is convincing: it persuades an expert reader that the result holds, with routine steps compressed into phrases like “clearly” and “it follows that.” A formal proof is valid: every inference is spelled out to the point where a machine with no mathematical intuition can confirm it.

That gap is where errors hide. Terence Tao’s January 2025 article in the Notices of the American Mathematical Society argues that interactive theorem provers are changing mathematicians’ practice while raising real epistemological questions about what a proof even is. The questions are not settled.

Paper proof versus formal proof

Property	Paper proof	Formal proof in Lean
Audience	An expert human reader	A machine with no intuition
Routine steps	Compressed (“clearly,” “it follows”)	Every step explicit
Error detection	Depends on the referee’s attention	Mechanical; a bad step will not compile
Time to produce	Baseline	Historically much longer
What errors remain possible	Logical gaps, unstated assumptions	Formalizing the wrong statement
Readability	Designed for humans	Hard to read; designed for the checker
Reusability	Cited by other papers	Importable as a library dependency
Verification cost	Weeks of expert time	Seconds, once formalized

The bottom two rows are why this matters commercially and scientifically. A formalized theorem is a reusable component; an informal one is a document someone has to re-read. And verification becomes nearly free after the expensive part is done.

The row I want parents to notice is the one about what errors remain possible. A Lean proof that compiles is logically airtight, but it only proves the statement you actually wrote. If you formalize the wrong theorem, Lean will happily verify it. That is exactly the same failure mode as code that passes its tests while solving the wrong problem.

The Liquid Tensor Experiment, in plain terms

In December 2020, Peter Scholze, a Fields medalist, did something unusual. He and Dustin Clausen had proved a theorem about “liquid vector spaces,” which would allow functional analysis and complex geometry to fit into their condensed mathematics framework. The argument was subtle enough that Scholze himself was not fully confident in it, so he publicly asked the formal-proof community to verify it.

The community took it up as the Liquid Tensor Experiment and worked in Lean. It was completed on July 14, 2022, about eighteen months later. Nature and Quanta Magazine both covered it.

Two things happened that are worth explaining to a teenager. First, one of the best mathematicians alive asked strangers to check his work because he was not sure. Second, they did, and it held. That is what intellectual honesty looks like at the top of a field, and it is a better story about mathematics than any “genius” narrative.

How to Teach Your Kid About Formal Proof

The concept is that a proof is a chain where every link must hold, not a story that sounds right.

Ages 5–8: The Because Game

Make a claim your child disagrees with, then justify it one step at a time, with them allowed to say “why?” after every step. “We should leave now.” Why? “Because the bus comes at 8.” Why does that matter? “Because if we miss it the next one is at 9.”

Then swap. They make a claim and you say “why?” until they run out. Running out is the lesson: you have reached an assumption, which is what an axiom is.

Ages 9–12: No Shortcuts Allowed

Give them a simple task with a rule: every instruction must be something you can do without thinking. Getting a glass of water becomes eight steps, not one. When they say “get a glass,” you ask “from where?”

This is exactly what formalization feels like. The tedium is the content: what feels like one step to a human is many steps to a machine, and each of those steps is a place an error could hide.

Ages 13+: Play the Natural Number Game

Send them to adam.math.hhu.de and start the Natural Number Game. It is the Lean 4 version of a game originally built by Kevin Buzzard and collaborators at Imperial College London, distributed under Apache 2.0, and it runs in the browser with no installation. Its README describes it plainly: “This is the lean4 version of the classical Natural Number Game… It uses the Lean4 Game Engine and is running live at adam.math.hhu.de.”

The game starts with Peano-style axioms and asks you to prove things you have known since you were five, like 2 + 2 = 4. Their first reaction will be that this is absurd. Around level four they will realize they never actually knew why 2 + 2 = 4, only that it does. That moment is the whole point.

Set a 45-minute limit the first time. The frustration is productive but it has a ceiling.

The question to ask: “Which step in your argument would a computer refuse to accept?”

Why this matters more in 2026

The verification bottleneck is now the field’s real constraint. Thomas Bloom, who maintains the Erdős problems database, told Quanta that AI-generated papers of 100 to 200 pages are arriving as claimed solutions and “no human has read it.”

Mechanical verification is the obvious answer, and it is not ready. Formalizing an informal proof still takes substantial work, sometimes more than writing the original. Quanta reports the tooling is being used sparingly: Nat Sothanaphan used the Aristotle prover to certify one proof’s logical coherence, and Liam Price used repeated checks with fresh model instances. Neither generalizes.

So the live question in mathematics right now is whether translation into formal systems can be automated. If it can, the bottleneck opens and AI-generated mathematics becomes trustworthy at scale. If it cannot, proofs will keep accumulating unverified. That is a genuinely open question, and a kid who has spent an afternoon in Lean understands the stakes better than most adults reading the headlines. Our companion piece on how mathematicians verify a 125-page AI proof lays out the three methods in use.

What to actually do at home

Treat “it compiled” as a separate question from “it’s right”

Whether it is Lean, a spreadsheet, or a Python script, the two questions are different. Does it run without error, and does it answer the question you meant to ask? Kids who internalize that distinction debug better for life.

Let them hit the wall

The Natural Number Game is designed to frustrate. A teenager who pushes through three levels learns something no explanation delivers: that “obvious” is not the same as “proven.”

Connect it to code they already write

If your kid writes any code, formal proof is a natural extension: a type system checking your program is the same idea as a proof assistant checking your argument. Our piece on computational thinking versus coding covers where the overlap sits.

Ask which step carries the weight

In any argument, one or two steps do the real work and the rest is bookkeeping. Finding the load-bearing step is how a referee reads a paper, and it is a skill that transfers to reading anything.

What not to do

Do not present Lean as a path to a career. Formal verification is a small field, and most people who learn it use it to think better, not to get hired. The honest pitch is that it is the clearest available lesson in what verification means, at a moment when that concept is doing a lot of work.

What to Watch For Over the Next 3 Months

• Week 4: Your teen finished at least one world of the Natural Number Game, or said out loud that they never knew why 2 + 2 = 4.
• Month 2 red flags: “It’s obviously true” as a substitute for an argument. That is the habit formal proof breaks.
• Month 3 self-check: Watch for progress on automated formalization. If translating informal proofs into Lean becomes substantially cheaper, the verification bottleneck loosens and AI mathematics changes character.

Frequently Asked Questions

What is Lean and who uses it?

Lean is an interactive theorem prover, now in its fourth version, used by mathematicians to write proofs that a computer checks mechanically. Its appeal comes largely from Mathlib, a community library with a large amount of undergraduate and graduate mathematics already formalized, so users can build on existing results.

Can a kid actually learn a proof assistant?

Yes, with the Natural Number Game. It runs in a browser at adam.math.hhu.de with no installation, is free and open source under Apache 2.0, and starts from the Peano axioms with goals as elementary as proving 2 + 2 = 4. It grew out of work by Kevin Buzzard and collaborators at Imperial College London.

Does Lean guarantee a proof is correct?

It guarantees every inference follows from the axioms and prior results, so a compiling Lean proof is logically valid. What it cannot guarantee is that you formalized the statement you meant. That is the same failure mode as code passing tests while solving the wrong problem.

Was the AI’s Erdős proof verified in Lean?

Not publicly. OpenAI says external mathematicians checked the proof and wrote a companion paper, which is human refereeing rather than formal verification. No Lean formalization of that proof has been announced.

Why doesn’t everyone formalize their proofs?

Because it takes much longer than writing an informal proof, sometimes longer than the original research. That cost is the reason the verification bottleneck exists, and whether automated formalization can reduce it is one of the open questions in the field.

---

About the author

Ricky Flores is the founder of HiWave Makers and an electrical engineer with 15+ years of experience building consumer technology at Apple, Samsung, and Texas Instruments. He writes about how kids learn to build, think, and create in a tech-saturated world. Read more at hiwavemakers.com.

---

Sources

1. Lean Prover Community. “Natural Number Game 4 (NNG4).” GitHub. https://github.com/leanprover-community/NNG4
2. Lean Community. (2022, July 14). “Completion of the Liquid Tensor Experiment.” https://leanprover-community.github.io/blog/posts/lte-final/
3. Tao, T. (2025, January). “Machine-Assisted Proof.” Notices of the American Mathematical Society, 72(1), 6–13. https://www.ams.org/notices/202501/rnoti-p6.pdf
4. Kakaes, K. (2026, August 3). “Why the legendary Erdős problems are falling to AI.” Quanta Magazine. https://www.quantamagazine.org/why-the-legendary-erdos-problems-are-falling-to-ai-20260803/
5. OpenAI. (2026, May 20). “An OpenAI model has disproved a central conjecture in discrete geometry.” https://openai.com/index/model-disproves-discrete-geometry-conjecture/
6. Jiang, E., Liang, X., et al. (with Tao, T.). (2026, July). “From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier.” arXiv:2607.07779. https://arxiv.org/pdf/2607.07779
7. Lean Game Server. “Lean 4 Games.” https://adam.math.hhu.de/