In my previous talk in this seminar, I discussed the construction of a class of structures originally due to Julia Knight. They are countable structures that have models of their Scott sentence of cardinality $\aleph_1$ but no larger, with additional nice homogeneity and algebraic properties. I mentioned that I was working on formalizing this result using Lean. With humility, as I am still far from an expert, I will give an introduction to Lean and Mathlib and show how I used it to formalize this result. I also hope to make some observation about the use of AI, how it helped me, and its strengths and limitations, as I used Claude Code extensively in this project. Finally, time permitted, I hope to outline a new construction of a variation of Knight's model for $\aleph_2$.