In 1977, Julia Knight produced a countable structure $K$ such that its Scott sentence has a model of cardinality $\aleph_1$ but no models of larger cardinality. In other words it "characterizes" $\aleph_1$. I will discuss how I have formalized the construction of Knight's model in the Lean 4 theorem prover with the Mathlib library. While I do plan to give a very basic introduction to Lean 4, I will spend most of my time discussing how this formalization project of an ad-hoc construction due to Knight lead to an interesting theory of a certain class of ordered algebraic objects. I also hope to discuss a project to construct the "right" analogue of Knight's model for cardinality $\aleph_2$, and how Lean 4 and AI are helping.