&gt; I prove mathematical properties purely for the sake of proving them<p>Good for you. I also think pure maths can be a fun diversion.<p>&gt; The fact that they have any bearing on the real world is a mildly interesting diversion.<p>Well, computer &quot;science&quot; is primarily an engineering discipline. It is therefore primarily, if not entirely, about having bearing on the real world.  (And even if it were a &quot;science&quot;, which it largely isn&#x27;t, that would still be the case).<p>&gt; Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof.<p>Given this frame of reference, your proof is of no relevance to software, which was exactly my point: yes, you can do these proofs, but they are largely irrelevant, and even if relevant <i>always</i> subsidiary to empirical evidence.<p>&gt; Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite.<p>How do you <i>know</i> that while these proofs reference the infinite, they are actually <i>applicable</i> to the infinite?  The answer is:  you don&#x27;t and you can&#x27;t.  You can only assume that the proof mechanisms you use actually do not break down.  Now I am certainly convinced (= I believe) that induction will continue to work for all N if I prove 1 and N -&gt; N+1, but I have only empirical evidence for small N to justify that belief. And if we found an M where it didn&#x27;t, what then?<p>And of course, there always have been (and probably always will be) &quot;proofs&quot; that were later shown not to be correct, just like physical &quot;laws&quot; that turned out not to be laws. All knowledge is contingent, <i>especially</i> all-quantified knowledge.<p>And I have to admit that I find the naive&#x2F;rigid belief (it is no more than that) in the absolute power of proofs...charming :-)