avewright/proofwiki-math huggingface dataset:
Theorem: Integers whose Divisor Count equals Cube Root

There are $3$ positive integers whose divisor count function equals its cube root:
{{begin-eqn}}
{{eqn | l = 1 = 1^3
      | o = :
      | r = \map {\sigma_0} 1 = 1
      | c = {{DCFLink|1}}
}}
{{eqn | l = 21 \, 952 = 28^3
      | o = :
      | r = \map {\sigma_0} {21 \, 952} = 28
      | c = {{DCFLink|21,952|21 \, 952}}
}}
{{eqn | l = 64 \, 000 = 40^3
      | o = :
      | r = \map {\sigma_0} {64 \, 000} = 40
      | c = {{DCFLink|64,000|64 \, 000}}
}}
{{end-eqn}}
{{OEIS|A066693}}

Proof:
Suppose $N = \map {\sigma_0} {N^3}$.
The case $N = 1$ is trivial.
Suppose $N$ is a prime power.
Write $N = p^n$.
By Divisor Count Function of Power of Prime:
:$N = \map {\sigma_0} {p^{3 n} } = 3 n + 1$
By Bernoulli's Inequality:
:$N = p^n \ge 1 + n \paren {p - 1}$
This gives us the inequality:
:$3 n + 1 \ge 1 + n \paren {p - 1}$
which can be simplified to:
:$3 \ge p - 1$
The only primes satisfying the inequality are $2$ and $3$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\sigma_0} {2^3}
      | r = 4
      | rr= > 2^1
}}
{{eqn | l = \map {\sigma_0} {2^6}
      | r = 7
      | rr= > 2^2
}}
{{eqn | l = \map {\sigma_0} {2^9}
      | r = 10
      | rr= > 2^3
}}
{{eqn | l = \map {\sigma_0} {2^{3 n} }
      | r = 3 n + 1
      | rr= < 2^n
      | c = for $n > 3$
}}
{{eqn | l = \map {\sigma_0} {3^3}
      | r = 4
      | rr= > 3^1
}}
{{eqn | l = \map {\sigma_0} {3^{3 n} }
      | r = 3 n + 1
      | rr= < 3^n
      | c = for $n > 1$
}}
{{eqn | l = \map {\sigma_0} {p^{3 n} }
      | r = 3 n + 1
      | rr= < p^n
      | c = for all $p > 3$
}}
{{end-eqn}}
Hence no prime powers satisfy the property.
Note that Divisor Count Function is Multiplicative.
To form an integer $N$ with our property, we must choose and multiply prime powers from the list above.
If we chose any $\tuple {p, n}$ with $\map {\sigma_0} {p^{4 n} } < p^n$, we must choose $2^m$ or $3^1$ in order for equality to possibly hold.
If $\tuple {2, 1}$ was chosen, $2^2 \nmid N$.
But $\map {\sigma_0} {2^3} = 4 \divides N$, which is a contradiction.
Suppose $\tuple {2, 2}$ was chosen.
Then $\map {\sigma_0} {2^6} = 7 \divides N$.
Then we must choose some $\tuple {7, n}$.
For $n = 1$, $\map {\sigma_0} {7^3} = 4$.
:$\map {\sigma_0} {2^6 \times 7^3} = 4 \times 7 = 28 = 2^2 \times 3$
:$\map {\sigma_0} {2^6 \times 7^3 \times p^{3 m} } = 28 \paren {3 m + 1} < 28 \times p^m$ for all $p \ne 2, 7$
For $n > 1$, $\map {\sigma_0} {2^6 \times 7^{3 n} } = 7 \paren {3 n + 1} < 4 \times 7^n$, a contradiction.
Suppose $\tuple {2, 3}$ was chosen.
Then:
:$\map {\sigma_0} {2^9} = 10 \divides N$
Then we must choose some $\tuple {5, n}$.
For $n = 1$, $\map {\sigma_0} {5^3} = 4$.
:$\map {\sigma_0} {2^9 \times 5^3} = 10 \times 4 = 40 = 2^3 \times 5$
:$\map {\sigma_0} {2^9 \times 5^3 \times p^{3 m} } = 40 \paren {3 m + 1} < 40 \times p^m$ for all $p \ne 2, 5$
For $n > 1$, $\map {\sigma_0} {2^9 \times 5^{3 n} } = 10 \paren {3 n + 1} < 2^3 \times 5^n$, a contradiction.
Suppose $\tuple {3, 1}$ was chosen.
Then $\map {\sigma_0} {3^3} = 4 \divides N$.
Then this case coincides the cases above.
Thus we have exhausted all cases.
{{qed}}
Theorem: Smallest Integer which is Product of 4 Triples all with Same Sum

The smallest integer which can be expressed as the product of $4$ different triplets of integers each of which has the same sum is:
{{begin-eqn}}
{{eqn | l = 25 \, 200
      | r = 6 \times 56 \times 75
}}
{{eqn | r = 7 \times 40 \times 90
}}
{{eqn | r = 9 \times 28 \times 100
}}
{{eqn | r = 12 \times 20 \times 105
}}
{{end-eqn}}

Proof:
We have:
{{begin-eqn}}
{{eqn | l = 6 \times 56 \times 75
      | r = \paren {2 \times 3} \times \paren {2^3 \times 7} \times \paren {3 \times 5^2}
      | c = 
}}
{{eqn | r = 2^4 \times 3^2 \times 5^2 \times 7
      | c = 
}}
{{eqn | l = 6 + 56 + 75
      | r = 137
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 7 \times 40 \times 90
      | r = 7 \times \paren {2^3 \times 5} \times \paren {2 \times 3^2 \times 5^2}
      | c = 
}}
{{eqn | r = 2^4 \times 3^2 \times 5^2 \times 7
      | c = 
}}
{{eqn | l = 7 + 40 + 90
      | r = 137
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 9 \times 28 \times 100
      | r = 3^2 \times \paren {2^2 \times 7} \times \paren {2^2 \times 5^2}
      | c = 
}}
{{eqn | r = 2^4 \times 3^2 \times 5^2 \times 7
      | c = 
}}
{{eqn | l = 9 + 28 + 100
      | r = 137
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 12 \times 20 \times 105
      | r = \paren {2^2 \times 3} \times \paren {2^2 \times 5} \times \paren {3 \times 5 \times 7}
      | c = 
}}
{{eqn | r = 2^4 \times 3^2 \times 5^2 \times 7
      | c = 
}}
{{eqn | l = 12 + 20 + 105
      | r = 137
      | c = 
}}
{{end-eqn}}
{{ProofWanted|It remains to be shown that this is the smallest such number with this property.}}
Theorem: 4 Integers whose Euler Phi Value is 10,368

:$\map \phi {25 \, 930} = \map \phi {25 \, 935} = \map \phi {25 \, 940} = \map \phi {25 \, 942} = 10 \, 368 = 2^7 \times 3^4$
where $\phi$ denotes the Euler $\phi$ function.

Proof:
{{begin-eqn}}
{{eqn | l = \map \phi {25 \, 930}
      | r = 10 \, 368
      | c = {{EulerPhiLink|25,930|25 \, 930}}
}}
{{eqn | l = \map \phi {25 \, 935}
      | r = 10 \, 368
      | c = {{EulerPhiLink|25,935|25 \, 935}}
}}
{{eqn | l = \map \phi {25 \, 940}
      | r = 10 \, 368
      | c = {{EulerPhiLink|25,940|25 \, 940}}
}}
{{eqn | l = \map \phi {25 \, 942}
      | r = 10 \, 368
      | c = {{EulerPhiLink|25,942|25 \, 942}}
}}
{{end-eqn}}
{{qed}}
The significance of this result escapes the author of this page.
Theorem: Fourth Power expressible as Sum of 6 Fourth Powers

$28 \, 561$ can be expressed as the sum of $6$ fourth powers:
:$28 \, 561 = 13^4 = 12^4 + 8^4 + 7^4 + 6^4 + 2^4 + 2^4$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = 12^4 + 8^4 + 7^4 + 6^4 + 2^4 + 2^4
      | c = 
}}
{{eqn | r = 20 \, 736 + 4096 + 2401 + 1296 + 16 + 16
      | c = 
}}
{{eqn | r = 28 \, 561
      | c = 
}}
{{eqn | r = 13^4
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Smallest Fermat Pseudoprime to Bases 2, 3, 5 and 7

The smallest Fermat pseudoprime to bases $2$, $3$, $5$ and $7$ is $29 \, 341$.

Proof:
{{ProofWanted|We have the list of Poulet numbers and Fermat pseudoprimes base $3$, but not of bases $5$ and $7$. Once we get those lists, we can find the numbers on the lists for both.}}
Theorem: Smallest Differences between Fractional Parts of Square and Cube Roots

Apart from $6$th powers, the value of $n$ less than $50 \, 000$ for which the difference between the fractional parts of $\sqrt n$ and $\sqrt [3] n$ is smallest is $30 \, 739$.
The next integer to produce a smaller difference above that is $62 \, 324$.

Proof:
{{begin-eqn}}
{{eqn | l = \sqrt {30 \, 739}
      | o = \approx
      | r = 175 \cdotp 32541 \, 17349
      | c = 
}}
{{eqn | l = \sqrt [3] {30 \, 739}
      | o = \approx
      | r = 31 \cdotp 32539 \, 66116
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sqrt {30 \, 739} - \sqrt [3] {30 \, 739}
      | o = \approx
      | r = 144 \cdotp 00001 \, 5123
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \sqrt {62 \, 324}
      | o = \approx
      | r = 249 \cdotp 64775 \, 18425
      | c = 
}}
{{eqn | l = \sqrt [3] {62 \, 324}
      | o = \approx
      | r = 39 \cdotp 64774 \, 02668
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sqrt {62 \, 324} - \sqrt [3] {62 \, 324}
      | o = \approx
      | r = 210 \cdotp 00001 \, 1576
      | c = 
}}
{{end-eqn}}
{{finish|This could be turned into a page where the sequence of $n$ for which this difference is smaller than for any smaller $n$.}}
Theorem: Smallest Triplet of Consecutive Integers each Divisible by Fourth Power

This triplet of consecutive integers has the property that each of them is divisible by a fourth power:
:$33 \, 614, 33 \, 615, 33 \, 616$
This is the smallest such triplet.

Proof:
{{begin-eqn}}
{{eqn | l = 33 \, 614
      | r = 14 \times 7^4
      | c = 
}}
{{eqn | l = 33 \, 615
      | r = 415 \times 3^4
      | c = 
}}
{{eqn | l = 33 \, 616
      | r = 2101 \times 2^4
      | c = 
}}
{{end-eqn}}
Each number in such triplets of consecutive integers is divisible by a fourth power of some prime number.
Only $2, 3, 5, 7, 11, 13$ are less than $\sqrt [4] {33 \, 616}$.
Theorem: Affine Group of One Dimension as Semidirect Product

Let $\map {\operatorname{Af}_1} \R$ be the $1$-dimensional affine group on $\R$.
Let $\R^+$ be the additive group of real numbers.
Let $\R^\times$ be the multiplicative group of real numbers.
Let $\phi: \R^\times \to \Aut {\R^+}$ be defined as:
:$\forall b \in \R^\times: \map \phi b = \paren {a \mapsto a b}$
Let $\R^+ \rtimes_\phi \R^\times$ be the corresponding semidirect product.
Then:
:$\map {\operatorname {Af}_1} \R \cong \R^+ \rtimes_\phi \R^\times$
where $\cong$ denotes (group) isomorphism.

Proof:
By definition, a (group) isomorphism is a (group) homomorphism which is a bijection.
Recall the definition of underlying set of $1$-dimensional affine group on $\R$:
:$S = \set {f_{a b}: x \mapsto a x + b : a \in \R_{\ne 0}, b \in \R}$
So the bijection $\psi: \map {\operatorname {Af}_1} \R \to \R^+ \rtimes_\phi \R^\times$ defined by $\map \psi {f_{a b} } = \paren {b, a}$ arises naturally.
It remains to show that $\psi$ is a (group) homomorphism:
Let $f_{a b}, f_{c d} \in \map {\operatorname {Af}_1} \R$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f_{a b} \circ f_{c d} } x
      | r = \map {f_{a b} } {\map {f_{c d} } x}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map {f_{a b} } { c x + d }
      | c = {{Defof|Affine Group of One Dimension}}
}}
{{eqn | r = a \paren {c x + d} + b
      | c = {{Defof|Affine Group of One Dimension}}
}}
{{eqn | r = \paren{ a \paren{c x } + a d } + b
      | c = {{Real-number-axiom|D}}
}}
{{eqn | r = a \paren{c x } + \paren{a d + b }
      | c = {{Real-number-axiom|A1}}
}}
{{eqn | r = \paren{a c } x + \paren{a d + b }
      | c = {{Real-number-axiom|M1}}
}}
{{eqn | r = f_{\paren {a c} \paren {a d + b} }
      | c = {{Defof|Affine Group of One Dimension}}
}}
{{end-eqn}}
Let $\tuple {b, a}, \tuple {d, c} \in \R^+ \rtimes_\phi \R^\times$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {b, a} \tuple {d, c}
      | r = \paren {b + \map {\map \phi a} d, a c}
      | c = {{Defof|Semidirect Product}}
}}
{{eqn | r = \paren {b + a d, a c}
      | c = Definition of $\phi$
}}
{{eqn | r = \paren {a d + b, a c}
      | c = Real Addition is Commutative
}}
{{end-eqn}}
So:
:$\map \psi {f_{a b} } \, \map \psi {f_{c d} } = \map \psi {f_{a b} \circ f_{c d} }$
So the bijection $\psi$ is a (group) homomorphism, and thus a (group) isomorphism.
{{qed}}
Theorem: Sequence of Consecutive Integers with Same Number of Divisors

The following sequence of consecutive integers all have the same number of divisors, that is, $8$:
:$40 \, 311, 40 \, 312, 40 \, 313, 40 \, 314, 40 \, 315$
This is the longest such sequence known.

Proof:
In the below, $\sigma_0$ denotes the divisor count function.
{{begin-eqn}}
{{eqn | l = \map {\sigma_0} {40 \, 311}
      | r = 8
      | c = {{DCFLink|40,311|40 \, 311}}
}}
{{eqn | l = \map {\sigma_0} {40 \, 312}
      | r = 8
      | c = {{DCFLink|40,312|40 \, 312}}
}}
{{eqn | l = \map {\sigma_0} {40 \, 313}
      | r = 8
      | c = {{DCFLink|40,313|40 \, 313}}
}}
{{eqn | l = \map {\sigma_0} {40 \, 314}
      | r = 8
      | c = {{DCFLink|40,314|40 \, 314}}
}}
{{eqn | l = \map {\sigma_0} {40 \, 315}
      | r = 8
      | c = {{DCFLink|40,315|40 \, 315}}
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = \map {\sigma_0} {40 \, 310}
      | r = 16
      | c = {{DCFLink|40,310|40 \, 310}}
}}
{{eqn | l = \map {\sigma_0} {40 \, 316}
      | r = 6
      | c = {{DCFLink|40,316|40 \, 316}}
}}
{{end-eqn}}
{{qed}}
Theorem: Pentagonal and Hexagonal Numbers

The sequence of positive integers which are simultaneously pentagonal and hexagonal begins:
:$1, 40 \, 755, 1 \, 533 \, 776 \, 805, 57 \, 722 \, 156 \, 241 \, 751, \ldots$
{{OEIS|A046180}}

Proof:
{{begin-eqn}}
{{eqn | l = 1
      | r = \dfrac {1 \paren {3 \times 1 - 1} } 2
      | c = Closed Form for Pentagonal Numbers
}}
{{eqn | r = 1 \paren {2 \times 1 - 1}
      | c = Closed Form for Hexagonal Numbers
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 40 \, 755
      | r = \dfrac {165 \paren {3 \times 165 - 1} } 2
      | c = Closed Form for Pentagonal Numbers
}}
{{eqn | r = 143 \paren {2 \times 143 - 1}
      | c = Closed Form for Hexagonal Numbers
}}
{{end-eqn}}
{{ProofWanted|It remains to be shown that these are the only such instances.}}
Theorem: Carmichael Number with 4 Prime Factors

$41 \, 041$ is the smallest Carmichael number with $4$ prime factors:
:$41 \, 041 = 7 \times 11 \times 13 \times 41$

Proof:
From Sequence of Carmichael Numbers:
{{:Carmichael Number/Sequence}}
The sequence continues:
:$\ldots, 29 \, 341, 41 \, 041$
We now investigate their prime factors:
{{begin-eqn}}
{{eqn | l = 561
      | r = 3 \times 11 \times 17
}}
{{eqn | l = 1105
      | r = 5 \times 13 \times 17
}}
{{eqn | l = 1729
      | r = 7 \times 13 \times 19
}}
{{eqn | l = 2465
      | r = 5 \times 17 \times 29
}}
{{eqn | l = 2821
      | r = 7 \times 13 \times 31
}}
{{eqn | l = 6601
      | r = 7 \times 23 \times 41
}}
{{eqn | l = 8911
      | r = 7 \times 19 \times 67
}}
{{eqn | l = 10 \, 585
      | r = 5 \times 29 \times 73
}}
{{eqn | l = 15 \, 841
      | r = 7 \times 31 \times 73
}}
{{eqn | l = 29 \, 341
      | r = 13 \times 37 \times 61
}}
{{eqn | l = 41 \, 041
      | r = 7 \times 11 \times 13 \times 41
}}
{{end-eqn}}
{{qed}}
Theorem: Smallest Sequence of 5 Consecutive Numbers which are Happy

The smallest sequence of $5$ consecutive integers all of which are happy numbers is:
:$44 \, 488, 44 \, 489, 44 \, 490, 44 \, 491, 44 \, 492$

Proof:
{{ProofWanted|Exhaustive enumeration? I'm afraid recreational mathematics of this kind bores me.}}
Theorem: Reciprocal of 21

:$\dfrac 1 {21} = 0 \cdotp \dot 04761 \, \dot 9$

Proof:
Performing the calculation using long division:
<pre>
   0.04761901...
  --------------
21)1.00000000000
     84
     --
     160
     147
     ---
      130
      126
      ---
        40
        21
       ---
        190
        189
        ---
          100
           84
          ---
          ...
</pre>
{{qed}}
Theorem: Smallest Fourth Power as Sum of 5 Distinct Fourth Powers

The smallest $4$th power which can be expressed as the sum of $5$ distinct $4$th powers is:
:$15^4 = 4^4 + 6^4 + 8^4 + 9^4 + 14^4$

Proof:
{{begin-eqn}}
{{eqn | l = 15^4
      | r = 50 \, 625
      | c = 
}}
{{eqn | r = 256 + 1296 + 4096 + 6561 + 38 \, 416
      | c = 
}}
{{eqn | r = 4^4 + 6^4 + 8^4 + 9^4 + 14^4
      | c = 
}}
{{end-eqn}}
By Fermat's Little Theorem, for $5 \nmid a$:
:$a^4 \equiv 1 \pmod 5$
For $5 \divides a$:
:$a^4 \equiv 0 \pmod 5$
Therefore in order for the equality to hold, one of the following must be true:
:The $4$th power on the {{RHS}} is not divisible by $5$, while exactly $1$ of the $5$ $4$th powers on the {{LHS}} is not divisible by $5$
:The $4$th power on the {{RHS}} is divisible by $5$, while all of the $5$ $4$th powers on the {{LHS}} is divisible by $5$
:The $4$th power on the {{RHS}} is divisible by $5$, while none of the $5$ $4$th powers on the {{LHS}} is divisible by $5$.
{{mistake|can we review whether we mean {{RHS}} and {{LHS}} throughout?}}
In the first two cases, there must be at least $4$ distinct $4$th powers divisible by $5$.
The smallest multiples of $5$ are $0, 5, 10, 15$.
Hence the $4$th powers on the {{LHS}} must exceed $15^4$.
Thus these cases cannot produce a smaller example.
This leaves us with the third case, where {{LHS}} is divisible by $5$.
Since $5^4 \ne 4^4 + 3^4 + 2^4 + 1^4 + 0^4$, we only need to check that $10^4$ is not a sum of $5$ distinct $4$th powers.
As $8^4 + 7^4 + 6^4 + 5^4 + 4^4 = 8674 < 10^4$, we must have $9^4$ on the {{RHS}}.
As $9^4 + 8^4 = 10657 > 10^4$, we cannot have $8^4$ on the {{RHS}}.
As $9^4 + 6^4 + 5^4 + 4^4 + 3^4 = 8819 < 10^4$, we must have $7^4$ on the {{RHS}}.
As $9^4 + 7^4 + 6^4 = 10258 > 10^4$, we cannot have $6^4$ on the {{RHS}}.
But $9^4 + 7^4 + 5^4 + 4^4 + 3^4 = 9924 < 10^4$.
Therefore $10^4$ is not a sum of $5$ distinct $4$th powers.
This proves that $15^4$ is the smallest $4$th power which can be expressed as the sum of $5$ distinct $4$th powers.
{{qed}}
Theorem: Boolean Interpretation is Well-Defined

Let $\LL_0$ be the language of propositional logic.
Let $v: \LL_0 \to \set {\T, \F}$ be a boolean interpretation.
Then $v$ is well-defined.

Proof:
By Language of Propositional Logic has Unique Parsability, $\LL_0$ is uniquely parsable.
Therefore, the Principle of Definition by Structural Induction can be applied to $\LL_0$.
By inspection, we see that the definition of the boolean interpretation $v$ follows the bottom-up specification of propositional logic.
Hence the Principle of Definition by Structural Induction implies that $v$ is well-defined.
{{qed}}
Theorem: Boolean Interpretation is Well-Defined

Let $\LL_0$ be the language of propositional logic.
Let $v: \LL_0 \to \set {\T, \F}$ be a boolean interpretation.
Then $v$ is well-defined.

Proof:
This is to be done by strong induction on the length of WFFs.
By definition of $v$ being a boolean interpretation, $\map v p$ is well-defined for all $p \in \PP_0$, the vocabulary of $\LL_0$.
A WFF of length $1$ has (trivially) a unique parsing sequence.
Consequently, only a single defining rule for $v$ as a boolean interpretation applies.
So the result holds for all WFFs of length $1$.
Now, suppose the result is true for all WFFs of length $k$ or less.
Let $\mathbf A$ be a WFF of length $k+1$.
There are two possibilities:
Suppose $\mathbf A = \neg \mathbf B$ for some WFF $\mathbf B$.
Then $\mathbf B$ is of length $k$, so by the induction hypothesis has a unique value $v (\mathbf B)$ no matter what parsing sequence is used.
So as $\map v {\mathbf A} = \map {f^\neg} {\map v {\mathbf B} }$, it follows that $\mathbf A$ likewise has a unique value.
Hence the result holds for $k + 1$ in this situation.
Suppose $\mathbf A = \paren {\mathbf B * \mathbf C}$ for some WFFs $\mathbf B$ and $\mathbf C$ and some connective $*$.
By Language of Propositional Logic has Unique Parsability, $*$ must be the unique main connective.
So $\mathbf B$ and $\mathbf C$ are both WFFs shorter than $k + 1$ and therefore by the induction hypothesis have unique values $\map v {\mathbf B}$ and $\map v {\mathbf C}$.
Since $\mathbf A = \paren {\mathbf B * \mathbf C}$ for a unique main connective $*$, it follows that:
:$\map v {\mathbf A} = \map {f^*} {\map v {\mathbf B}, \map v {\mathbf C} }$
is well-defined.
Hence the result holds for $k + 1$ in this situation.
So the result follows by the Second Principle of Mathematical Induction.
{{qed}}
Theorem: Pandigital Pairs whose Squares are Pandigital

The elements of the following pandigital pairs of integers each have squares which are themselves pandigital:
:$\left({35 \, 172, 60 \, 984}\right), \left({57 \, 321, 60 \, 984}\right), \left({58 \, 413, 96 \, 702}\right), \left({59 \, 403, 76 \, 182}\right)$
{{OEIS|A085545|order = first}}

Proof:
{{begin-eqn}}
{{eqn | l = 35 \, 172^2
      | r = 1 \, 237 \, 069 \, 584
      | c = 
}}
{{eqn | l = 60 \, 984^2
      | r = 3 \, 719 \, 048 \, 256
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 57 \, 321^2
      | r = 3 \, 285 \, 697 \, 041
      | c = 
}}
{{eqn | l = 60 \, 984^2
      | r = 3 \, 719 \, 048 \, 256
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 58 \, 413^2
      | r = 3 \, 412 \, 078 \, 569
      | c = 
}}
{{eqn | l = 96 \, 702^2
      | r = 9 \, 351 \, 276 \, 804
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 59 \, 403^2
      | r = 3 \, 528 \, 716 \, 409
      | c = 
}}
{{eqn | l = 76 \, 182^2
      | r = 5 \, 803 \, 697 \, 124
      | c = 
}}
{{end-eqn}}
{{ProofWanted|It remains to be shown there are no further such pairs.}}
Theorem: Language of Propositional Logic has Unique Parsability

The language of propositional logic $\LL_0$ has unique parsability.

Proof:
It is to be demonstrated that each WFF arises by a unique rule of formation from the bottom-up specification of propositional logic.
The rules $\mathbf W : TF$ and $\mathbf W : \PP_0$ need no further treatment.
From inspection of the first character it is clear that the remaining $\mathbf W : \neg$ and $\mathbf W : Op$ cannot yield the same WFF.
What remains is to establish uniqueness in applying $\mathbf W : \neg$ and $\mathbf W : Op$.
For $\mathbf W : \neg$, this means to consider:
:$\mathbf A = \neg \mathbf B = \neg \mathbf C$
from which it is immediate that $\mathbf B = \mathbf C$.
Lastly, for $\mathbf W : Op$, we have the following lemma:
Theorem: Powers of 2 not containing Digit Power of 2

$2^{16} = 65 \, 536$ is the only known power of $2$, up to $2^{31 \, 000}$, whose digits do not contain $1$, $2$, $4$ or $8$.

Proof:
This has been demonstrated by an exhaustive search.
{{qed}}
Theorem: Construction of Regular 65,537-Gon

It is possible to construct a regular polygon with $65 \, 537$ sides) using a compass and straightedge construction.

Proof:
From Construction of Regular Prime $p$-Gon Exists iff $p$ is Fermat Prime it is known that this construction is possible.
{{ProofWanted}}
Theorem: There are no Odd Unitary Perfect Numbers

No unitary perfect numbers exist which are odd.

Proof:
Let $n$ be an odd number with prime decomposition $n = p_1^{a_1} \cdots p_k^{a_k}$.
By Sum of Unitary Divisors of Integer, the sum of its unitary divisors is $\ds \prod_{1 \mathop \le i \mathop \le k} \paren {1 + p_i^{a_i} }$.
To be a unitary perfect number, this must be equal to $2 n$.
Since each $p$ is odd, each $1 + p_i^{a_i}$ is even.
Hence $\ds \prod_{1 \mathop \le i \mathop \le k} \paren {1 + p_i^{a_i} }$ is divisible by $2^k$.
Since $n$ is odd, $2 n$ is divisible by $2$ but not $4$.
Thus $k = 1$.
So $n$ is a prime power.
By Sum of Unitary Divisors of Power of Prime, the sum of its unitary divisors is $1 + n$.
This cannot be equal to $2 n$, since $n > 1$.
Therefore there are no unitary perfect numbers which are odd.
{{qed}}
Theorem: Automorphic Numbers with 5 Digits

The only $5$-digit automorphic number which does not begin with a zero is $90 \, 625$.

Proof:
We have:
:$90 \, 625^2 = 8 \, 212 \, 8 \mathbf {90 \, 625}$
thus demonstrating it is automorphic.
By Automorphic Numbers in Base 10, the only other possible candidate is $6^{5^4}$.
However:
:$6^{5^4} \equiv 09 \, 376 \pmod {10^5}$
begins with a zero.
Hence there are no others.
{{qed}}
Theorem: Kaprekar's Process on 5 Digit Number

Let $n$ be a $5$-digit integer whose digits are not all the same.
Kaprekar's process, when applied to $n$, results in one of the following $3$ cycles:
:$53 \, 955 \to 59 \, 994 \to 53 \, 955$
:$61 \, 974 \to 82 \, 962 \to 75 \, 933 \to 63 \, 954 \to 61 \, 974$
:$62 \, 964 \to 71 \, 973 \to 83 \, 952 \to 74 \, 943 \to 62 \, 964$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = 95 \, 553 - 35 \, 559
      | r = 59 \, 994
}}
{{eqn | l = 99 \, 954 - 45 \, 999
      | r = 53 \, 995
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 97 \, 641 - 14 \, 679
      | r = 82 \, 962
}}
{{eqn | l = 98 \, 622 - 22 \, 689
      | r = 75 \, 933
}}
{{eqn | l = 97 \, 533 - 33 \, 579
      | r = 63 \, 954
}}
{{eqn | l = 96 \, 543 - 34 \, 569
      | r = 61 \, 974
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 96 \, 642 - 24 \, 669
      | r = 71 \, 973
}}
{{eqn | l = 97 \, 731 - 13 \, 779
      | r = 83 \, 952
}}
{{eqn | l = 98 \, 532 - 23 \, 589
      | r = 74 \, 943
}}
{{eqn | l = 97 \, 443 - 34 \, 479
      | r = 62 \, 964
}}
{{end-eqn}}
{{ProofWanted|It remains to be shown that all $5$-digit numbers end up here}}
Theorem: Tableau Extension Lemma/General Statement

Let $\mathbf H'$ be another finite set of WFFs.
Then there exists a finished finite propositional tableau $T'$ such that:
$(1):\quad$ the root of $T'$ is $\mathbf H \cup \mathbf H'$;
$(2):\quad$ $T$ is a rooted subtree of $T'$.

Proof:
Let $T_{\mathbf H'}$ be the finite propositional tableau obtained by replacing the hypothesis set $\mathbf H$ of $T$ with $\mathbf H \cup \mathbf H'$.
By the Tableau Extension Lemma, $T_{\mathbf H'}$ has a finished extension $T'$.
By definition of extension, $T_{\mathbf H'}$ is a rooted subtree of $T'$.
But $T_{\mathbf H'}$ and $T$ are equal when considered as rooted trees.
The result follows.
{{qed}}