Are there rigorous formulation and proof of the pigeonhole principle?
Yes and no. A fairly precise statement of the pigeonhole principle would be:
If $A$ and $B$ are sets, and $A$ has more elements than $B$, and $f$ is a function $A\to B$, then $f$ is not injective.
Can it be proved? That depends. In particular, what does "$A$ has more elements than $B$" mean? In the usual development of set theory we use this phrase to mean the same as "$A$ has larger cardinality than $B$", which again means
There is an injective function $B\to A$, but there is no injective function $A\to B$.
So if we use that as our definition, the pigeonhole principle is not a matter of proof -- instead it is part of the definition of what it means for one set to be larger than the other.
Of course, once we define natural numbers, we might want to prove a "finite pigeonhole principle":
If $m$ and $n$ are naturals, and $m>n$, and $A$ has $m$ elements and $B$ has $n$ elements, and $f$ is a function $A\to B$, then $f$ is not injective.
Then all we have to do is to prove this from a definitions of "has $m$ elements" and "$m<n$".
The first of these is fairly easily done, because in the usual development, the natural number $m$ is represented by the set $\{0,1,2,\ldots,m-1\}$ and "has $m$ elements" means to be in bijective correspondence by precisely that set. So when we strip away those bijections, what we have to prove is that if $m>n$ and $f:m\to n$, then $f$ is not injective.
This would be trivial (and pointless) if we're using the cardinality definition of what $m>n$ means -- so even though that is the most common choice, let's assume that we want to define $m>n$ to mean "there is a natural $a$ such that $n+a+1=m$.
The actual content of the proof now is to show that these two competing definitions of $>$ agree! Of course we first need to define addition, but once we have done that, it is a fairly simple matter of induction.
First we prove that $|m+1|>|m|$ (as cardinals) for all $m$. The base case $m=0$ is easy. $0$ is the empty set, so there is no function for $1\to 0$ at all, so in the impossible case that we get one, we can safely claim it will be non-injective.
For the induction case, assume that $|m+1|>|m|$ and we need to show that $|m+1+1|>|m+1|$. Let $f: (m+1+1)\to(m+1)$ be given, and let $b=f(m+1)$
$$g:(m+1)\to m : x \mapsto\begin{cases}f(x) & \text{when }f(x)\ne m \\ b & \text{when }f(x)=m \end{cases}$$
Then by the induction hypothesis $g$ is not injective, so there is $p$ and $q$ with $g(p)=g(q)$. If $f(p)=f(q)$ then $f$ is not injective, and we're done. Otherwise $f(p)\ne f(q)$, but this can only be the case if one of them is $m$ and the other is $b$. But then either $f(p)$ or $f(q)$ equals $f(m+1)$, and $f$ is again not injective.
Now to complete the proof, we just have to handle the case where $a\ne 0$ in $|m+a+1|>|m+1|$. By this time we hopefully know that addition is commutative and associative, so $m+a+1=m+1+a$. And so if we have $f:(m+a+1)\to (m+1)$, then it is also $((m+1)+a)\to(m+1)$, and its restriction to $(m+1)$ is not injective. A restriction of an injective function would itself be injective, so $f$ is not injective. (Whew!).
(... except that we also ought to prove along the way that $p+a\subseteq p$ with the standard representation of the natural numbers; otherwise restricting the last $f$ to $(m+a)$ doesn't make sense).
For a third option, we could also have said that $m>n$ means that $n\in m$ for the set representation of the numbers. That would need a different proof from the induction above.
But all in all, these proofs are not very enlightening about the pigeonhole principle. Intuitively I would say that the pigeonhole principle is itself at least as obvious as it is that $n+a+1=m$ is a good definition of $m>n$. So what the proof actually proves could be argued to be just that the $n+a+1$ definition is reasonable. And this would also be the case for the $n\in m$ alternative.
Let $X$ be a (finite) set of order $n$, and let $S_1, \dots, S_m\subset X$ with $\bigcup S_i = X$. The pigeonhole principle then asserts that if $m < n$, then some $\#S_i > 1$. For if all $\#S_i \leq 1$, then $n = \#X \leq \#S_1 + \cdots + \#S_m \leq m$.
A proof by induction on $m$ is quite flexible in terms of how it's formalised, that is to say "basically the same proof" will work in different systems. Outline:
Base case $m = 1$, if more than one item is put in exactly one box, then that box contains all the items. So at least one box has more than one item.
Suppose for the inductive step that whenever more than $k$ items are placed in exactly $k$ boxes then at least one box contains more than one item.
Now, place more than $k+1$ items in exactly $k+1$ boxes. Consider two cases of what is in the first box:
- More than one item. Then one of the boxes (namely the first) contains more than one item.
- 1 or 0 items. Then the remaining items (of which there are more than $k + 1 - 1 = k$) were placed in the other boxes (of which there are exactly $k$) and therefore by the inductive hypothesis one of the boxes contains more than one item.
So either way, at least one box contains more than one item and the induction is complete.
Note: if feeling brave, take the base case as $m = 0$, and state/show that it is not possible to put more than $0$ items into $0$ boxes at all. Proofs by induction where the base case is vacuously true are more fun ;-)
Now, how to rigorously formalise this proof depends firstly on how you formalise "putting items in boxes", and secondly on how you formalise the natural numbers. You could do the latter either by axiomatizing a Peano system or using the common set-theoretical construction. You could do the former either by defining a partition of a set with $n$ elements, where there are $m$ sets in the partition, so $x \in y$ means "item $x$ is in box $y$". Or (equivalently) by a function from a set of size $n$ to a set of size $m$, where $f(x) = y$ means "item $x$ is in box $y$". Or some other way. But in order to talk about the size of a set, we need a formalisation of "size" too. Developing that and showing the necessary properties is potentially the first two or more lectures of a "foundations of mathematics" course, and if anyone can fit it in a reasonably-sized answer to this question then I tip my hat to them! I'm reminded of Russell and Whitehead's Principia Mathematica, where page 379 contains proposition 54.43, together with the remark "From this proposition it will follow, when arithmetical addition has been defined, that $1 + 1 = 2$". A fully formal statement and proof of even the simplest thing can be a major undertaking, it's all a matter of where you start.
I reckon you can fill out the details in my proof by induction in any formalism you're inclined to choose, because all I need is the principle of induction, the ability to consider the first box, the ability to consider "the remaining items" after discounting 0 or 1 of them, and a lemma I snuck past without stating, that if you have $n$ items and set one aside then there are $n-1$ others. That can be proved by induction and used, together with some arithmetic, to prove the two claims in the inductive step about the numbers of the remaining items and remaining boxes.
There's probably some really good way to formalise these features (plus anything else I used without noticing), and then show that any logical system that has those things proves its own version of the Pigeonhole Principle, but I don't have the theory to do that myself. Similarly, each of the other answers here uses certain properties of the system it works in, and wherever those properties can be assumed or proved, that proof of the Principle works.