What makes maths beautiful?
I had a run-in with this issue once.  Many years ago, when working on a program verification system, I had to show that two theorem provers (Boyer-Moore and Nelson-Oppen) were working on compatible theories. If that was botched, the system
could prove false statements. So I undertook to prove, in Boyer-Moore theory, the &quot;axioms&quot; of arrays used in the Nelson-Oppen prover. McCarthy defined four classic axioms for arrays, and here are the first two.<p><pre><code>    p=r ⇒ read(write(a, p, v), r) = v

    ¬(p=r) ⇒ read(write(a, p, v), r) = read(a, r)
</code></pre>
This just says that if you store v at a[p], and then read it back, you get what you put there, and you don&#x27;t change any other elements.<p>So I set this up in Boyer-Moore notation.<p><pre><code>    (PROVE-LEMMA SELECT-OF-STORE-1 (REWRITE) 
        (IMPLIES (AND (arrayp A) (NUMBERP I)) 
                 (EQUAL (selecta (storea A I V) I) V)))

    (PROVE-LEMMA SELECT-OF-STORE-2 (REWRITE) 
        (IMPLIES (AND (arrayp A) (NUMBERP I) (NUMBERP J) (NOT (EQUAL I J))) 
                 (EQUAL (selecta (storea A I V) J) (selecta A J))))
</code></pre>
But Boyer-Moore theory is constructive; everything must have a definition that can be evaluated as a function. So I had to define arrays and the &quot;selecta&quot; and &quot;storea&quot; functions so that this would work. I could do this by defining an array as a list of (subscript, value) tuples.<p><pre><code>    (ADD-SHELL UNDEFINED-OBJECT UNDEFINED UNDEFINEDP ())

    (ADD-SHELL array-shell 
        empty-array 
        array-recognizer 
        ((array-elt-value (NONE-OF) UNDEFINED) 
         (array-elt-subscript (ONE-OF NUMBERP) ZERO) 
         (array-prev (ONE-OF array-recognizer) empty-array)))
</code></pre>
This is simply a structure definition for a list.  An array-shell has an array-elt-value, an array-elt-subscript, and
array-prev, which is the rest of the elements. &quot;array-shell&quot; is the constructor, &quot;empty-array&quot; is essentially &quot;nil&quot; for
this type, and &quot;array-recognizer&quot; is a predicate which is true for objects of type array-shell.<p>For array equality to work, the list of tuples had to be ordered by subscript, so that two arrays with the same values would always have the same representation.  So selecta and storea are complicated. selecta is a recursive lookup in a list:<p><pre><code>    (DEFN selecta (A I) 
        (IF (EQUAL (array-elt-subscript A) I) 
                   (array-elt-value A) 
                   (IF (EQUAL (array-prev A) (empty-array)) 
                       (UNDEFINED) 
                       (selecta (array-prev A) I))))

</code></pre>
Store into array is ugly, because it&#x27;s an update of an ordered list.<p><pre><code>    (DEFN storea (A I V)
        (IF (NOT (arrayp A))                   
            (empty-array) 
            (IF (NOT (NUMBERP I))
                A 
                (IF (EQUAL A (empty-array)) 
                    (IF (EQUAL V (UNDEFINED)) 
                        (empty-array) 
                        (array-shell V I (empty-array))) 
                    (IF (EQUAL (array-elt-subscript A) I) 
                        (IF (EQUAL V (UNDEFINED)) 
                            (array-prev A) 
                            (array-shell V I (array-prev A)))
                        (IF (LESSP (array-elt-subscript A) I) 
                            (IF (EQUAL V (UNDEFINED)) 
                                A 
                                (array-shell V I A)) 
                            (array-shell 
                                (array-elt-value A)
                                (array-elt-subscript A) 
                                (storea (array-prev A) I V))))))))
</code></pre>
This recursive function is complicated enough that it needs a lemma to help with proof of termination.<p><pre><code>    (PROVE-LEMMA storea-is-sound (REWRITE) 
        (implies (and (arrayp a) 
            (not (equal a (empty-array)))) 
            (lessp (count (array-prev a)) (count a))))
</code></pre>
This says that the array-prev list component of a is always shorter than a. The Boyer-Moore prover must prove
termination for all defined functions, which it does by examining any recursive call and proving that there is
a measure defined on the arguments which is a smaller nonnegative integer. For the easy cases, the prover can do
this automatically, but sometimes you have to define a lemma to help it. The lemma, of course, also has to be proved.<p>So, given all that, the Boyer-Moore theorem prover could be turned loose to grind out proofs of the rules for arrays.
It took about 45 minutes of grinding in 1982 on a 1 MIPS VAX 11&#x2F;780.
You can rerun it now. Here&#x27;s the prover, which requires clisp.[1]. Here&#x27;s the entire set of definitions and theorems we used for program verification.[2]. Read the instructions at [1], and get the system up to where it&#x27;s done &quot;boot-strap&quot;. Then load the file at [2].  Long, detailed, human-readable explanations of the proof steps are displayed.  The entire proof run for all those basic theorems takes about a second, and that&#x27;s probably mostly scrolling.<p>So, having rigorously proved the &quot;axioms&quot; for arrays from first principles, I submitted a paper to JACM. The reviewer comments I got back were mainly about the uglyness of the approach. All that case analysis! One comment was that the reviewer was upset about having a proof that ugly at the foundations of computer science. The paper was rejected.<p>The reason it&#x27;s ugly is that it doesn&#x27;t get to use set theory. Informally, a set is a collection whose order does not matter. &quot;Order does not matter&quot; is not a meaningful concept in strict Boyer-Moore theory.  If order matters, there are many cases to prove, stemming from all those IF statements in the definitions.<p>A generation later, fewer mathematicians would be bothered by this form of &quot;uglyness&quot;.  But back then, machine proofs were
so rare that this was considered awful. Also, now that computers can do this in a second, complaining that it&#x27;s too 
complicated seems whiny.<p>[1] <a href="https:&#x2F;&#x2F;github.com&#x2F;John-Nagle&#x2F;nqthm" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;John-Nagle&#x2F;nqthm</a>
[2] <a href="https:&#x2F;&#x2F;github.com&#x2F;John-Nagle&#x2F;pasv&#x2F;blob&#x2F;master&#x2F;src&#x2F;work&#x2F;temporaryrulebase.lisp" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;John-Nagle&#x2F;pasv&#x2F;blob&#x2F;master&#x2F;src&#x2F;work&#x2F;temp...</a>