All examples that I can come up with confirm that If "A → B" is correct, "¬B → ¬A" is correct, but is it possible to rigorously prove that negating a true implication always will result in another true implication?
Please note that I have no background in philosophy, except for mathematics (up to Calculus) if you count that as a branch of philosophy, or formal logic. As such, I may have trouble understanding certain jargon.
Er, I think there's several ways to answer this, but I'm going to give two thoughts that might help organize it for you.
First, there's a problem with the sentence you wrote about negation:
t is it possible to rigorously prove that negating a true implication always will result in another true implication?
The problem is that it's not clear what "negating a true implication" means here. Negating a true statement yields a false statement. If you look, ¬B → ¬A is not the "negation" of A → B. Given the relation A → B, there's at least three distinct possible operations:
Second, each of these operations has a different relationship to the truth of A → B. Starting with the easiest:
The other operations are actually more complicated. It is not simply the case that they are opposites. Instead, we have to look at the effects of negating each piece independently. The easy way to do that is with a truth table that maps all the possibilities (it does so by considering every possible value for every variable. Given that we have two variables {A,B} with two possibilities each {T,F}, we have 4 rows):
A | B | ¬A | ¬B | A → B | ¬A → ¬B | ¬B → ¬A | ¬(A → B)
T T F F T T T F
T F F T F T F T
F T T F T F T F
F F T T T T T F
The columns for "A → B" and "¬B → ¬A" are perfectly identical. This means they are the same logically.
Returning to your question, any two logical operators with exactly the same truth table mean the same thing and can be traded. Thus, "contraposition" rather than being the negation of "implication" is implication -- just written in a different way.
Does it contain two negations? Yes, but they don't negate the whole.
I don't disagree with Virmaior's answer, but it is worth making the point that the validity of contraposition depends on which logic you are using. If you are assuming classical logic, and if the '→' connective is intended to denote material implication, then contraposition is valid, which is to say that A → B entails ¬B → ¬A and vice versa. This can be demonstrated syntactically and semantically. The syntactic demonstration is to construct a proof, e.g. using natural deduction, while the semantic demonstration can be achieved by constructing truth tables and showing that the two sentences share the same values. This works for classical logic because it is bivalent, which is to say that it assumes there are only two truth values, and any sentence that is not true is false and any sentence that is not false is true.
If we choose to move away from classical logic, things get more complicated. Intuitionistic logic, for example, is not bivalent (nor indeed n-valent for any n). We can still construct a proof that A → B entails ¬B → ¬A but not vice versa. But without bivalence we cannot simply appeal to a boolean truth table to get a semantic demonstration; we would need something more complex, such as a Heyting algebra.
More importantly, there are logics in which contraposition is not valid at all. For example, in David Lewis' logic of counterfactual conditionals, A ◻→ B does not entail ¬B ◻→ ¬A. Also, in Ernest Adams' probability logic it may be highly probable that B given A, but not highly probable that ¬A given ¬B. So in general, when speaking of ordinary English conditionals, one cannot always expect contraposition to be safe. A noteworthy corollary is that in both the Lewis and Adams logics, while contraposition is not valid, modus tollens is valid. Some accounts of logic incorrectly run together contraposition with modus tollens and treat them as the same thing. While both are classically valid, they do not agree across all logics.
It is moderately ambiguous what 'not A' means. In the simplest formal systems (like the truth tables in @virmaior's answer) negation is just a convention of reversing truth values. But formalism is meant to reflect meaning, not dictate it.
Informally, negation is about avoiding asserting two contradictory things at the same time in the same way. So it is common to define 'not A' to mean 'asserting A produces a contradiction with other things we know'.
(Aside for the picky: This is even the formal definition in many systems that take various paradoxes and the 'groundedness' of deductions seriously, like intuitionism and paraconsistency, where we attempt to expand discovery out from what we know, instead of assuming the world itself is automatically consistent, like in the informal logic of mathematics. And it is equivalent in Classical logic to the simple flipping of truth values, because all true things are equivalent and we know some of them.)
Then when A implies B and B produces a contradiction with other things we know, asserting A makes B true, which produces a contradiction with other things we know...
So not B implies not A. And this rule of contraposition is true across a broad range of logics with a more formal, but more fragile semantics, including the Classical logic most of us use, though as @Bumble notes, not all sorts of logic.