  We present {\lambda}ert, a type theory supporting refinement types with
explicit proofs. Instead of solving refinement constraints with an SMT solver
like DML and Liquid Haskell, our system requires and permits programmers to
embed proofs of properties within the program text, letting us support a rich
logic of properties including quantifiers and induction. We show that the type
system is sound by showing that every refined program erases to a simply-typed
program, and by means of a denotational semantics, we show that every erased
program has all of the properties demanded by its refined type. All of our
proofs are formalised in Lean 4.
