A computerised proof checker is much less likely to have a mistake than a typical computer program - or a mathematical proof - because it's extremely simple.