Can all math results be formalized and checked by a computer?

Can all math results, that have been correctly proven so far, be formalized and checked by a computer? If so, what type of logic would need to be used there?

I've heard that the first-order logic is not expressive enough: certain facts can not be expressed in it, and sometimes proofs can be given, but they have asymptotically large size (not just merely syntactically inconvenient).

First, the good news:

There is a strong belief among mathematicians, particularly among mathematical logicians, that nearly all (correct) proofs in the literature could be formalized to the point that a computer could completely verify the proof.

There are many automated theorem verifiers ("proof assistants") that have been developed for this purpose. Recent developments include completely verified proofs of the Prime Number Theorem (two independent formalizations), the Jordan Curve Theorem, and the Four Color Theorem. It is certainly possible to completely formalize nontrivial mathematics.

The bad news is that

The process of taking a proof in a journal and converting it to a proof that can be verified by computer is tedious, arduous, and non-trivial.

Even though a proof assistant program takes proofs in a high-level format as input, the format is still much more detailed and verbose than a natural language proof would ever be. Moreover, the standard foundational systems (such as ZFC) are particularly difficult to work with to actually write formalized proofs.

Avigad (2007) reported about the proof of the Prime Number Theorem, which was written in the much more convenient system Isabelle, that:

"The five-line derivation of the Mobius inversion formula in Section 3.1 translates to about 40 lines, and the proof of the form of the Selberg symmetry formula discussed there, carried out in about two-and-a-half pages in Shapiro’s book, takes up about 600 lines, or 13 pages. These ratios are more typical."

He also reported

"This process stabilized, however, and towards the end [I] found that [I] could formalize about a page of Shapiro’s text per day."

So, although we all believe it is possible to fully formalize a proof, the effort required with current technology makes it impractical. Most top-tier research mathematicians can assimilate much more than one page of a textbook in a full working day. Perhaps technology will improve.

There is also a question of purpose. Some (perhaps influenced by technology) view computer verified proofs as a goal to work towards. But others, including Bourbaki, have viewed it as a distraction. Many of the latter kind feel that the purpose of proofs is to communicate ideas with other mathematicians. While computer verified proofs have some additional certainty, the form in which they are written is not at all suitable for conveying ideas to other mathematicians. After all, what mathematicians are usually interested to see is not only the "proof", but also the "idea" or "method" that underlies the proof, because that is what can be used to prove other theorems.