The year was 2021, and I was in charge of tutoring my sister—who was in secondary school at the time—helping her with some basic geometry problems. Through this, I really felt her struggle to express her thinking.
Rigorousness is very hard to enforce on children, it’s almost unnatural to ask them to be so precise and write down the “recipes” they used to come up with their proofs.
Elementary textbooks of my country started out with Euclidean geometry, and I vividly remember myself also being confused at an early age. It is not geometry itself that’s hard, but rather the weirdness and vastness in the way it’s taught. Something is wrong with trying to pretend that we are so rigorous while we are not that rigorous.
They started out with boxes of theorems and postulates. As a child, those words sound really foreign. We never use them in day-to-day conversation. My dad (who was a math teacher) did explain them to me, but at that age, I could only get that those two things were somehow different by definition. Only much later, when I turned into a logic fanatic, did I grasp the idea behind those words. To see these terms as part of a thinking framework.
Instead of making sense out of that early mess (which is rather quite impossible), my teacher made a good choice by emphasizing useful geometry formulas. These became cheat sheets (the list) that we carried into exams.
As I progressed through school, it became apparent that there would be more lists, and how difficult it was to remember them all. At some point, my brain decided it did not feel any happier adding any more of those propositions, and my math knowledge became full of cheese holes.
Accumulated through the years, you have yourself a stack similar to those listicles you find online: 20 important inequalities you should remember, a trigonometry table, 15 differentiation formulas, etc. While these lists are indeed useful and people expect using them to become second nature, they also expect that you just accept those tools as first principles and carry on.
With those lists in my hands, math really feels random. There is no real structure underneath, and we never really spent time revisiting how these lists were created.
I have never given school any credit for being a reliable measure of one’s worth, but it just feels a little hollow to think that when one says “good at math,” they are referring to the scoring metrics that rely so much on memorization and mechanical computation.
Gödel showed us that there is freedom in math.
It’s 2025, folks! We have computers that can help kids learn interactively! Let them play with the rules, break them, and see for themselves why each rule is a necessity.
Don’t skip the important bits that teach us how to think.
2021 is also the year I discovered Logicomix and started playing with Lean. I realized that these proof assistants have an amazing ability to straighten out my messy thoughts and can systematically help me build up my library of math facts. I found incredible joy in adding yet another proven fact to my collection.
I couldn’t use Lean to teach my sister, however, because (1) she did not know how to code, and (2) Lean is built on the complex Dependent Type Theory.
I did attempt to build an early prototype of a simpler proof assistant to convince myself that there was some value there. It is a graphical, point-and-click proof assistant, in which you can click on a “fact,” then click on a pattern, and the machine combines them to create new facts.
For example, you can pick a fact saying “AB has the same length as CD,” and match it with the first clause of the rule “if xy has the same length as pq, and pq has the same length as mn, then xy has the same length as mn.” Then the fact “if CD has the same length as mn, then AB has the same length as mn” would be added to your library.
You can build your proof fact by fact until you reach the desired construction, like building an equilateral triangle where all three equality facts are added to your library.
That core mechanic was fun for me. I definitely didn’t know what I was trying to build at that time and had some difficulties with adding in the axiom schema of continuity. It was put on the shelf because of that.
Fast forward four years, I just undusted it last week and have already made some progress on both the underlying language and the interface.
In high school, when I was struggling with remembering all the derivatives, I fortunately happened to stumble upon the concept of dual numbers.
A dual number is similar to a complex number; it has the form of
where
\(\epsilon \neq 0 \quad \text{but} \quad \epsilon^2 = 0\)
The second part should stand out a bit. Wouldn’t the only number that satisfies x^2=0 be 0?
That is because we are not operating in the normal real number system; we are operating in the new dual number system (a ring extension) that follows its own consistent logic. This is similar to how, if we need the imaginary number i, we could use the complex number system to be consistent with x^2 = -1.
In this new dual number system, there exists a number ε. You can think of this as a “super small number, smaller than any real number, but more than 0.” It is so “small” that when you multiply it by itself, it vanishes (ε^2 = 0). It is perfect for representing small, infinitesimal changes.
Due to this algebraic nature, you can use it to prove common derivatives algebraically. For example, to find the derivative of x^3, we normally have to use the Limit Definition of a Derivative in standard calculus:
\(f'(x) = \lim_{h \to 0} \frac{f(x+h) - f(x)}{h}\)
This involves expanding the cubic and carefully canceling out the h terms before taking the limit.
With ε, there is no tricky “approaching zero” logic. You replace that limit with the fixed algebraic rule ε^2=0, and the derivative just “pops out” as the coefficient of ε.
Since ε^2 = 0, the equation simplifies to:
\((x + \epsilon)^3 = x^3 + 3x^2\epsilon\)
So the derivative of x^3 is 3x^2!
We can form an intuition by interpreting how ε works:
Imagine a physical cube with side length x. Its volume is x^3.
If you grow each side by an infinitesimal amount ε, you aren’t just adding “volume”; you are painting a new “skin” onto the cube.
The 3 Plates: To grow the cube in three directions (length, width, height), you have to add three flat square plates. Each plate has an area of x^2. Total area: 3x^2ε.
The Edges and Corners: Where these plates meet, there are thin rods xε^2 and a tiny corner cube ε^3. In our dual number world, these are so microscopic that they vanish. The growth of the edges and corners are insignificant compared to the surface.
The dual number system tells us that the “speed” at which the volume grows is exactly the surface area of the faces being pushed out.
If you want to find more about this, you might find this introduction helpful.
So, by adding a new set of rules to our toolkit, we have a very “intuitive” understanding of derivatives through symbol manipulation and to me it just feels a bit more natural than the limit definition. Of course you don’t have to agree with this, and that’s the point! You should have your own set of rules that you are comfortable with.
Of course, the new system may not always be 100% consistent with the mainstream one, but that’s okay. It’s just there to helps us build understanding, and if you want it to be consistent, you can try hard and adjust the rules to make it so.
I’m making a graphical proof assistant that runs as a web app. In the app, you can open a world with some facts and use them to construct new facts within that world. For example, in this world here I have three facts:
There is a point A
There is a point B
There is a rule that if you are given two points, a and b, you can construct a new segment
To construct the segment, kids can drag and drop the two facts there, and the system will add a new fact to their world: segment AB.
Underneath is a rewriting system, and I’ve encoded Euclidean geometry and proved some propositions using it, but there is still some work left to do. For example, allowing proofs to be portable and reusable, so that if our users manage to construct an object (like an equilateral triangle), they don’t have to rebuild it from scratch every time but can “re-execute the program.” There are also opportunities to reveal certain hidden assumptions and rules that do not necessarily need to hold.
The idea is to have an underlying language like Isabelle/Pure: a small logic kernel not built on any specific theory as a foundation, but capable of expressing those theories if needed. It might be more convoluted to write proofs, but it would be easier to understand and use for kids (graphically through the UI).
Another feature I want to ship is the Canvas: when you hover over a fact, it would highlight that object geometrically. This is specific to geometry, but it’s important to show lines, circles, squares, and so on when learning this topic.
One might argue: is there a point at all? After all, what’s the point of teaching anything apart from doing correct calculations, since the end goal is to put that knowledge to “good use”?
To lay the bricks at the right angle!
In my country especially, I get it—raising a generation skilled in calculation might seem more practical than raising one with a high chance of becoming crackpots.
I just think there should be a way to let kids explore, be creative, and find the artistry in math. Right now, there’s almost no space for that—they’re being fed dry bread. I’m just trying to find the butter (said the person who choked). And maybe, if we can sprinkle a little butter on top, we can make learning math not just useful, but joyful.
If anyone can come up with a good argument—such as how these things are actually very important, or how improving logic would translate to better math performance—do share it over :)