 Its official target is “formalism” or “metamathematics”. But (as we have noted) “formalism” doesn’t just mean “formalism” proper, as this term is usually understood in the Philosophy of Mathematics. For Lakatos “formalism” includes not just Hilbert’s programme but also logicism and even intuitionism. Formalism sees mathematics as the derivation of theorems from axioms in formalised mathematical theories. The philosophical project is to show that the axioms are true and the proofs valid, so that mathematics can be seen as the accumulation of eternal truths. An additional philosophical question is what these truths are about, the question of mathematical ontology.