There’s this anecdote about Ramanujan, one of the brightest mathemacian who lived shortly between 1887 and 1920:
I remember once going to see him when he was ill at Putney. I had ridden in taxi cab number 1729 and remarked that the number seemed to me rather a dull one, and that I hoped it was not an unfavourable omen. "No," he replied, "it is a very interesting number; it is the smallest number expressible as the sum of two cubes in two different ways."
So apparently:
We can verify this by hand, and it’s only a matter of time before you reach the same result.
We can also write some code, or… we can throw the heavy machine and use a solver for this. Z3 is great at this, and the book SAT/SMT by example is a great introduction on the topic of theorem proving. It comes with complete examples, so it’s great if maths
Given a description of the problem, Z3 can minimize the solution for us. That’s the awesome part: all you have to do is proprerly describe the problem, and z3 will solve it.
Let’s take an example with a system of equations:
from z3 import *
# This program solves the following system of equation
# 3x + 2y - z = 1
# 2x - 2y + 4z = -2
# -x + 0.5y - z = 0
# example from https://yurichev.com/writings/SAT_SMT_by_example.pdf
x, y, z = Reals('x y z')
s = Solver()
s.add(3*x + 2*y - z == 1)
s.add(2*x - 2*y + 4*z == -2)
s.add(-x + 0.5*y -z == 0)
print(s.check())
print(s.model())
We only said that our problem involves x, y and z, we said there are 3 equations linking them, but we never implemented an algorithm to solve that. And in a few seconds, it will display the solution
[z = -2, y = -2, x = 1]
So, we can do the same thing to
from z3 import *
a, b, c, d = Ints('a b c d')
cube_sum = Int('cube_sum')
s = Optimize()
s.add(a > 0)
s.add(b > 0)
s.add(c > 0)
s.add(d > 0)
s.add(a < 20)
s.add(b < 20)
s.add(c < 20)
s.add(d < 20)
s.add(And(cube_sum == (a * a * a) + (b * b * b)))
s.add(And(cube_sum == (c * c * c) + (d * d * d)))
s.add(And(a != c, a != d, b != c, b != d))
s.minimize(cube_sum)
s.check()
m = s.model()
print(m)
def debug(u, v):
print("{}^3 + {}^3 = {}".format(m[u].as_long(), m[v].as_long(), m[u].as_long() ** 3 + m[v].as_long() ** 3))
debug(a, b)
debug(c, d)
And again, it finds the solution.
$ python cube_sum.py
[d = 12, c = 1, b = 10, a = 9, cube_sum = 1729]
9^3 + 10^3 = 1729
1^3 + 12^3 = 1729
Here it is, $1729 = 9^3 + 10^3 = 1^3 + 12^3$.
Interestingly, you need to setup some upper bounds to the problem:
s.add(a < 20)
s.add(b < 20)
s.add(c < 20)
s.add(d < 20)
Without those bounds, the search space is way to big and you won’t find a solution in a reasonnable time. That’s an issue because it means you have to know beforehand some elements about the search space, which you may not always have.