The end goal is to formalize the famous textbook Model Theory: An Introduction by David Marker.
- Right know, the aleph0 categoricity of the theory of dense linear orders are proved. The essential part of the proof, which is the back-and-forth argument, was already in Mathlib but it was in terms of the instances LinearOrder, Countable etc. We just provided the dictionary to carry the proof to the language of model theory.