Mathematics is fully deductive (so it is not strictly speaking a science - it is not empirical, but it's own kind of discipline, like logics, if you don't consi

Mathematics is fully deductive (so it is not strictly speaking a science - it is not empirical, but it's own kind of discipline, like logics, if you don't consider that part of mathematics), so replication can be attempted by machine, and as the authors wrote proof-checkers find more and more mistakes. A water-tight proof essentially is the trace or log showing a series of mechanical deductive steps. But because journals publish human proofs, one of the following cases can arise: - A proof can be wrong and the underlying conjecture can still be true (i.e. a theorem). - A proof can be wrong and the conjecture can be false - these kinds of errors need to be corrected with utmost urgency, because they lead to follow-up downstream errors. - A proof can be right and recognized as such by peers, in which case it gets published and everybody is happy. - A proof can also be right and be contested by peers. This is when proofs have gaps that are "obvious" to some, but not believed by others. Because a proof is a sequence of steps that are either previously derived or self-evident, and people simply differ what they consider self-evident (as an aside, in school I was criticized in maths for "skipping steps" and in English for "jumping thoughts"; to me it seemed obvious where things were going but the teachers obviously needed "comments to the code", so I learned to insert baby steps, and everyone was happy). Because of the last case, it is important to get down to the most formal, fine-grained, nitpicky, atomic level, so everyone can agree that each micro-step is self-evident, and thankfully we can dedicate this to machines nowadays (provers like the "Isabelle" system - https://www.cl.cam.ac.uk/research/hvg/Isabelle/ https://www.cl.cam.ac.uk/research/hvg/Isabelle/), at least to an extent. Ironically, that's not how real proofs in mathematics journals look like at all. They're written in prose, and often written in a surprisingly "meta" style (we had algebra lectures where the professor talked about "colored roosters" and how they behave, which is the name of some structure in the algebraic sub-field of Ramsey theory).