Type inference is a critical part of the compiler for strongly typed languages like OCaml. The type inference engine manages competing priorities. On the one hand, its performance is crucial for LSP responsiveness. On the other, type safety relies on the correctness of type inference. OCaml's type inference includes many complex performance-related optimizations, and even more have been suggested. However, formalization efforts have been lagging behind. We examine the OCaml levels system, an implementation technique for generalization in which high-profile bugs have been found. We introduce Smart Levels, a type inference algorithm for a Hindley-Milner calculus that combines existing level optimizations in OCaml with a previously proposed scheme for deferred level updates. We formalize these optimizations and provide a roadmap to proving them correct.