run magma on sections3.mag, for instance by typing

load "section3.mag";
  or
iload "section3.mag";

in magma, and see that every claim in section 3 is verified.