Lean for the Inept Mathematician

This repository contains source files for a number of articles or posts aimed at explaining bite-sized mathematical concepts with the help of the Lean Theorem Prover and mathlib, its library of mathematics.

The authors of these posts are themselves not mathematicians (so corrections or pointers are most welcome!). We aim to learn ourselves, and in the process, perhaps explain a thing or two about mathlib to any who find it useful.

The name, self-deprecatingly (for those of us who choose to apply it to ourselves), is an homage to the wonderful Lean for the Curious Mathematician event held annually by the Lean community for the last few years.