Through much of the 20th century, questions of mathematical rigour were passed off to logicians and philosophers—working mathematicians have been, for the most part, content to work with an intuitive definition of proof
This notion works when each step of a proof is transparent, and can be examined by all. Proof is then just a process of reducing one big, non-obvious step, to a bunch of small, obvious ones. However, if a computer is used to make this reduction, then the number of small, obvious steps can be in the hundreds of thousands—impractical even for the most diligent mathematician to check by hand. Critics of computer-aided proof claim that this impracticability means that such proofs are inherently flawed. However, its defenders point out that some theorems that many mathematicians consider to have been proved in the classical manner also have proofs which are so long as to be uncheckable.
The most famous case of this is something called the classification of finite simple groups. These are abstract objects with certain mathematical properties; the claim is that, over a 30-year span in a series of papers totalling some 15,000 pages, all possible such objects were enumerated. Though the mathematical consensus is that the classification (nicknamed the “enormous theorem”) is complete, there are sceptics who point out that the dispersed proof is essentially unverifiable.