The mathematician Hilbert formulated the ideal that in mathematics every true mathematical statement would get its deductive proof, and in the first four decades of the 20th century mathematicians and logicians spend a lot of time on establishing systems of proof to do this and to clarify the whole notion of mathematical deductive proof.

The clarification succeeded, and several new and useful formats for mathematical proofs were found, notably Gentzen's sequent systems and techniques of natural deduction and Beth's semantic tableaux.

The notion that all mathematically true statements in a system of mathematical assumptions could and would eventually find their deductive proof was refuted by Gödel, who proved that in mathematical systems that are strong enough to contain arithmetic, one can formulate statements in the language of the system that assert their own unprovability, and that therefore cannot be validly proved in the system (if it is consistent) and must be intuitively true (since the statement asserts what is the case). See Gödel's Theorems.

Modern introductions to mathematical logic contain normally expositions of several techniques of proof. Kleene's 'Mathematical Logic' is one such exposition, that explains both axiomatic proofs, and proofs by natural deduction and by sequents. Smullyan's 'First Order Logic' surrects the whole basic theory of first-order logic using tableaux methods. Gentzen's 'Untersuchungen über das logische Schlieszen' is still worth reading and can be found in many collections (such as Berka & Kreiser). And one textbook with elegant and fargoing systems is Schütte's 'Proof Theory'.