When are formal proofs worth the effort?

Posted on 3 December 2020 by John

Formal verification of theorems takes a lot of work. And it takes more work where it is least needed. But the good news is that it takes less effort in contexts where it is needed most.

Years of effort have gone into formally verifying the proofs of theorems that no one doubted were correct. For example, a team worked for six years to formally verify the proof of the odd-order theorem in group theory.

Mathematical proofs are fallible, but it’s rare for a proof to be accepted that reaches a wrong conclusion. Flaws in proofs are much more likely to be gaps in reasoning than to be arguments in favor of false statements. And the more people who study a proof, the more likely it is that flaws will be found and fixed.

The return on investment for formal verification is highest for theorems that are the opposite of the odd-order theorem, theorems that are obscure and shallow rather than famous and deep.

For example, suppose you want to prove that a complex set of security protocols doesn’t have any gaps. Your problem is obscure in that only your company cares about it. You don’t have the assurance that would come from thousands of mathematicians around the world reviewing your work.

But on the plus side, your security rules are logically shallow. These rules may be too complicated to hold in your head, but they can be formally specified with far less effort than some mathematical object like a Möbius strip. In general, discrete things like if-then rules are much easier to formalize than continuous things like real numbers.

Mathematicians choose to study things they have some intuition for, and that intuition is often correct even when the reasoning around it is logically incomplete. But businesses are often faced with complex problems they did not chose and problems for which no one has much intuition, such as proving that a complex circuit does what it’s supposed to do, or that an encryption protocol didn’t neglect some edge case. That’s where the ROI on formal methods is greatest.

A cross product in 7 dimensions

Posted on 2 December 2020 by John

Can you define something like cross product of three-dimensional vectors in other dimensions? That depends on what you mean by a product being “like” the familiar cross product. In [1] Walsh lists several properties of the cross product, and proves that there exists a product with these properties only in dimensions 1, 3, and 7.

$\begin{align*} \mathbf{a} \times \mathbf{b} &= -(\mathbf{b} \times \mathbf{a}) \\ \mathbf{a} \times (\mathbf{b} + \mathbf{c}) &= (\mathbf{a} \times \mathbf{b}) + (\mathbf{a} \times \mathbf{c}) \\ \lambda(\mathbf{a} \times \mathbf{b}) &= (\lambda \mathbf{a}) \times \mathbf{b} \\ \mathbf{a} \cdot (\mathbf{a} \times \mathbf{b}) &= 0 \\ |\mathbf{a} \times \mathbf{b}|^2 &= |\mathbf{a}|^2 |\mathbf{b}|^2 - (\mathbf{a}\cdot \mathbf{b})^2 \end{align*}$

Walsh points out that given the first four properties, the last is equivalent to saying that the product of two orthogonal unit vectors is another unit vector.

In one dimension, define the cross product of any two “vectors” to be 0. This trivial cross product only works in one dimension because there are no orthogonal unit vectors in one dimension.

To define his cross product in seven dimensions, Walsh partitions the seven components of a vector into groups of 3, 1, and 3 and treats the groups of size three as three dimensional vectors. Then he defines the product as follows:

$\begin{align*} (\mathbf{a}_1, \lambda_1, \mathbf{b}_1) \times (\mathbf{a}_2, \lambda_2, \mathbf{b}_2) \equiv\,\,& \Big(\lambda_1 \mathbf{b}_2 - \lambda_2 \mathbf{b}_1 + \mathbf{a}_1\times \mathbf{a}_2 - \mathbf{b}_1\times \mathbf{b}_2, \\ & \phantom{\big(}\,\,\mathbf{a}_2 \cdot \mathbf{b}_1 - \mathbf{a}_1\cdot \mathbf{b}_2 ,\\ & \phantom{\big(}\,\,\lambda_2 \mathbf{a}_1 - \lambda_1 \mathbf{a}_2 - \mathbf{a}_1\times \mathbf{b}_2 - \mathbf{b}_1 \times \mathbf{a}_2 \Big) \end{align*}$

On the left side, × means the cross product in seven dimensions. On the right side, × means the ordinary cross product in three dimensions.

Although this product satisfies the properties of cross product given at the top of the post, Walsh points out that his product does not satisfy the Lie identity

$\mathbf{a} \times (\mathbf{b} \times \mathbf{c}) + \mathbf{c} \times (\mathbf{a} \times \mathbf{b}) + \mathbf{b}\times(\mathbf{c} \times \mathbf{a}) = \mathbf{0}$

that the ordinary cross product satisfies. This shows that the Lie identity is not a consequence of the identities above.

[1] Bertram Walsh. The Scarcity of Cross Products on Euclidean Spaces. The American Mathematical Monthly, Feb., 1967, pp. 188-194

Density of square-free numbers, cube-free numbers, etc.

Posted on 1 December 2020 by John

An integer n is said to be square-free if no perfect square (other than 1) divides n. Similarly, n is said to be cube-free if no perfect cube (other than 1) divides n.

In general, n is said to be k-free if it has no divisor d > 1 where d is a kth power [1].

As x gets larger, the proportion of numbers less than x that are k-free approaches 1/ζ(k). That is

$\lim_{x\to\infty} \frac{Q_k(x)}{x} = \frac{1}{\zeta(k)}$

where Q_k(x) is the number of k-free positive integers less than or equal to x and ζ is the Riemann zeta function.

The values of ζ at even integers are known in closed form. So, for example, the proportion of square-free numbers less than x approaches 6/π² since ζ(2) = π²/6. For odd integers the values of ζ must be calculated numerically.

Once you have a theorem that says one thing converges to another, it’s natural to ask next is how fast it converges. How well does the limit work as an approximation of the finite terms? Are there any bounds on the errors?

In [2] the authors give new estimates the remainder term

$R_k(x) = Q_k(x) - \frac{x}{\zeta(k)}$

Python code

Let’s play with this using Python. The code below is meant to be clear rather than efficient.

    from sympy import factorint

    def kfree(n, k):
        exponents = factorint(n).values()
        return max(exponents) < k

    def Q(k, x):
        q = 1 # because 1 is not k-free
        for n in range(2, x+1):
            if kfree(n, k):
                q += 1
        return q

    print(Q(4, 1000000))

This says Q₄(1,000,000) = 923,939.

So Q₄(10⁶)/10⁶ = 0.923939. Now ζ(4) = π⁴/90, so 1/ζ(4) = 0.9239384….

We have R₄(10⁶) = 0.597 and so in this case R is quite small.

(If we didn’t know ζ in closed form, we could calculate it in python with scipy.special.zeta.)

Month: December 2020

When are formal proofs worth the effort?

A cross product in 7 dimensions

Related posts

Density of square-free numbers, cube-free numbers, etc.

Python code

More posts involving Riemann zeta