Proving myself (Part I)

I wrote some code this week. At first glance, it either looks confusing, or nothing really special. And yeah, you're right. It isn't anything special. But to me, it is kinda special. In a way, this code is a small but significant step in breaking through a wall that has haunted me for 20+ years. I am finally able to understand a concept that I felt that I'd never understand. And I was finally able to take the skills I know very well and use them elsewhere, to help me get through this wall.

Here it is:

import Mathlib

example (a b c d : ℤ) : (a + b) + (c + d) = (a + d) + (b + c) := by
	rw [← add_assoc]
	rw [add_comm a b]
	rw [add_assoc]
	rw [add_comm c d]
	rw [← add_assoc]
	rw [add_assoc b a d]
	rw [add_comm b (a + d)]
	rw [add_assoc]

(And if you'd like to play with this code a bit, you can.)

But I'm getting ahead of myself.

What is that code, anyway?

You're looking at Lean 4 code. It's a programming language that is not only used for writing software, but also to write and verify (mathematical) proofs. Math and computer science folks might also be familiar with rocq, which is somewhat similar.

If you are familiar with math, you might see what is being done here, and if you have some programming (and Lean 4) experience, you're likely thinking that there must be a better way to write this proof. Yes, there is, and yes, I have written it in a cleaner way. But I kept this version as a reminder of a small moment in time. And I'll come back to it in a later post. But before we get there, let's talk about my experiences with math.

The abbreviated math story

I'll skip to around the mid-2000s, as my experiences with math were pretty uninteresting until that point. I went through the usual: from basic arithmetic to pre-algebra up until 10th grade or so. I learned all about functions, variables, graphs, coordinate systems, and the like. Boring stuff (which I learned was a problem, but we'll get to that later). I bring up 10th grade, as that was the year where I felt my first true challenge in math: geometry.

Up until my 10th grade geometry class, math was nothing more than a toolset that I learned how to use well enough to pass tests. I could solve for x when given x + 3 = 5 all day long without a problem. I could plot points and find the slope of lines without a second thought. I spent enough time learning multiplication tables where I could give you 12 * 11 in record time. But then geometry came, and while there was still a decent amount of calculation to do, there was something new that came up: proofs.

Now, it wasn't enough to just plug numbers into variables and memorize a bunch of stuff. I also had to explain, step-by-step, how and why things are the way they are. I won't go into much detail here, as I did manage to pass geometry without a lot of problem. But something about thinking of math in this way made me feel uncomfortable - as if this was unnatural. I didn't know why it was necessary to do all this work when we can just take these concepts at face value - like we were already doing. But at the time I thought that this would be the last time I'd be seeing proofs.

Of course, the rest of high school involved more algebra. And getting into college, I wasn't fortunate enough to do particularly well on my math placement exam (foreshadowing), so I ended up taking college algebra and trigonometry courses my first year of college, and getting solid grades there. And when the second year came, it was time for calculus. To say I was unprepared for it would be an understatement.

Calculus

In hindsight, I can look back and laugh at how much I struggled with calculus, and have some pride in the fact that I was eventually able to get through my I and II courses, and graduate! But it took a long time to get there.

I could go into great detail on how hard it was to learn and understand the many concepts that make up calculus, but it's not necessary. Calculus is one of the first roadblocks for many people in engineering and science fields, and it is one of the courses that causes quite a few folks to change course (I was an English major for a time...). But why is that?

A common line I've heard when it comes to difficulty with calculus is: "you're not bad at calculus, you're just bad at algebra". And I was one of the people that was confused at this, because I generally did fine with algebra. The only math class I struggled with in the past was geometry (foreshadowing, again), so I didn't understand what the issue was. And I wouldn't for many more years. But eventually, I came to realize I was good at using algebra, not understanding algebra. And more deeply, I could use certain concepts of math just fine, but I didn't often understand them.

Suffice to say, lacking this understanding of mathematical concepts and having to build on top of a shaky foundation with new concepts (limits, derivatives, integrals, and a TON of functions and rules to remember) made calculus feel almost impossible to understand. It also didn't help that my college professors didn't always make it clear what things like derivatives and integrals were - just how they can be used.

Unfortunately, I wasn't able to pass calculus I on the first try. Or the second... but I eventually did.

Someone made it easy

I don't remember who recommended me this book, or when, but during a prolonged break from school, I was pointed towards a book named Calculus Made Easy. I was skeptical at first, but after reading the first chapter, I saw the vision.

The first chapter explained derivatives and integrals in a way that made sense immediately. It managed to do in two pages what repeating a Calculus I course couldn't.

And after a few weeks of reading and practice questions after work, I finished reading the book and worked through most of its exercises. I finally understood the concepts well enough to feel comfortable with explaining the concepts to other folks!

The book does a great job breaking down the concepts of a typical Calculus I course, but it isn't perfect. It doesn't speak about limits at all, and it also does expect you to have a good grasp of algebraic concepts. It also doesn't touch on proofs very much. But it was enough to help me get past my required math courses in college, and get past the major roadblock to my computer science degree. Eventually, my grasp of calculus was good enough to even use it in other courses (physics included). I got my degree, found a job, had a few more jobs afterwards, wrote a lot of code, and lived happily ever after... or at least until 2025.