Simple formally verified compiler in Lean

Computer checked proofs that a compiler is correct are important for increasing the confidence in programs. This report presents a simple compiler and a proof that the compiler is correct for terminating evaluations using the interactive theorem prover Lean, based on Concrete Semantics: with Isabelle/HOL. The compiler compiles a simple imperative language defined by a big-step semantics, to a stack machine defined by a small-step semantics. The proof is done by induction on the big-step semantics. Because the compiler, semantics and proofs are all written in and check by Lean, we can have great confidence that the proof, and by extension, the compiler is correct. The aim is that the proof is understandable for people new to program (and especially compiler) verification, and that it can serve as good entry point. In particular the correctness proof of arithmetic expressions is explained in detail