Many useful mathematical proofs can be derived based on proving the impossibility of a contradictory assumption. I can try to disprove the triangle angle sum theorem (that the sum of the three angles in any triangle is 180) by attempting to draw a triangle that contradicts that assumption. I may begin by drawing two 90 degree angles. In doing so, I instead demonstrate that the 2 unconnected lines will never intersect in 2D space, and thus the figure cannot be triangle. This is a useful step along the way of formally proving that the sum of angles in any triangle is 180. My attempt at drawing an impossible figure can help visualize exactly why such a figure is impossible.
This suspension of constraint enforcement is easy on pen and paper. I can attempt to draw whatever I wish. However, there is no easy way to experiment in this way with modern mathematical software. How do you formalize a proof by contradiction in software that has these constraints pre-programmed?
That the internal angles of a triangle on the Euclidean plane add up to pi, can be derived directly, without resorting to proof by contradiction. (Hint: Draw a parallel line to one of the edges, which passes through the vertex not contained in that edge.)
Also, a proof by contradiction of an equality is unsatisfactory in constructive mathematics, because, in general, you can't go from “that A and B are not equal implies a contradiction” to “A and B are equal”. (This would require equality to be decidable.)
This suspension of constraint enforcement is easy on pen and paper. I can attempt to draw whatever I wish. However, there is no easy way to experiment in this way with modern mathematical software. How do you formalize a proof by contradiction in software that has these constraints pre-programmed?