Bordism theory is perhaps the simplest example of an extraordinary homology theory. Proving the Eilenberg-Steenrod axioms is particularly simple (unlike for e.g. singular homology). It is used e.g. in the proof of the Hirzebruch signature theorem, which is one ingredient for the existence of exotic spheres. I have been working on formalising the basics of (unoriented) bordism theory: this is both beautiful mathematics and an interesting test of mathlib's differential geometry library. I will explain the main ideas, and speak about the insights and challenges from formalisation: as so often, finding the right definition is less obvious than it seems. This is ongoing work. No prior knowledge in differential geometry will be assumed.