Introduction

For a long time now, I've considered starting a weblog, and over the years I have had many people suggest that I start one, but the question that is always unanswered is: "What do I write?" I've decided to make this a blog about the subject that has consumed my thoughts for the past year, and that's Metamath.

For those who don't know, Metamath is a proof language for writing mathematical proofs which can be checked by an associated verification program, and I have been using Metamath to write proofs and submit them to the database, called set.mm, since around the beginning of 2013. Back then most of what I did was revise old theorems to make them more efficient or avoid usage of the axiom of choice or clean them up in some way, and then in February 2014 I was made aware of Freek Wiedijk's Formalizing 100 Theorems page, which tracks the formalization of 100 of the most famous theorems in mathematics, and I decided to make it my goal to prove all of these.

When we first started tracking our progress, there were 19 theorems already proven, and over the past 8 months 15 more have been proven. Of those, 12 were my work. This includes such theorems as

• The Basel problem: $\sum_{n=1}^\infty\frac1{n^2}=\frac{\pi^2}6$ (basel),
• Bertrand's postulate: $n\in\Bbb N\to\exists p\in\Bbb P:n<p\le 2n$ (bpos),
• Lagrange's theorem for groups: $G$ finite group, $H\subseteq G$ subgroup implies $|H|$ divides $|G|$, (lagsubg),

and many others. I hope in later articles to talk a little more about the way these proofs are being done, and also highlight my latest work, and talk more generally about metamath and mmj2, the program I use (and develop) as a proof assistant to make the proofs. My current project is a proof of the Fundamental Theorem of Calculus, which has required a lot of work on defining a (Lebesgue) integral and derivative. But for now, welcome to my blog.