#computer-assisted-proof

? If a theorem was checked by a program I can’t check by hand, do I know it is true?

My day job involves writing code that a proof assistant checks line by line. So this is not a hypothetical question for me. Two famous cases. The four colour theorem was proved in 1976 by Appel and Haken, with a computer checking…