Number fields and their rings of integers are fundamental objects in algebraic number theory. Computational information on these objects is available in computer algebra systems and databases. To make these values available to formalization in Lean 4, without tediously redoing existing work, we developed a variety of certificates that allow Lean to efficiently verify the outcome of computations. In particular I will focus on computing and certifying the ring of integers. The work of this talk is joint with Alain Chavarri Villarello and Sander Dahmen at Vrije Universiteit Amsterdam.