 The soundness of this definition amounts to the belief that a published proof can, in principle, be converted into a formal proof.However, outside the field of automated proof assistants, this is rarely done in practice.A classic question in philosophy asks whether mathematical proofs are analytic or synthetic.