Computation in research: experimental mathematics and verification

Computers have changed how mathematics is discovered, checked and even proved. Gauss, as a teenager in the 1790s, spent hours counting primes in blocks of a thousand and guessed from his tables that their density near \(x\) is about \(1/\ln x\), the statement that became the prime number theorem. Today the same kind of exploration takes seconds, and computation also enters proofs directly: the four-colour theorem, the Kepler conjecture and the Boolean Pythagorean triples problem were all settled with essential help from computers. This lesson treats computation as a research tool with its own standards. It covers how to use computers to discover, how to make computations trustworthy, how to present them in a thesis, and how to think about new tools, including AI systems, that have arrived in the last few years.

Three roles for computation

Computation plays three distinct roles in mathematical research, and it helps to keep them apart.

Exploration. Computing examples to find patterns and formulate conjectures, as Amara did in lesson 1. Here speed and flexibility matter more than rigour: a quick script that produces a suggestive table is worth more than a polished program that is never written. Errors in exploratory code waste time but do not end up in theorems, provided every conjecture is later proved or verified properly.

Verification. Testing a conjecture over a large range, checking a proof's computational claims, or confirming a formula numerically. Here correctness is essential, because the results will be quoted. Verification code should be clear, tested on cases with known answers and, ideally, checked by an independent method.

Proof. Some theorems are proved by reducing them to a finite but enormous computation that only a computer can perform. The proof then consists of a mathematical reduction plus a computation, and its reliability depends on both. Such proofs are now accepted by the mathematical community, but they demand extra care: the code must be available, the computation reproducible, and ideally the result checked by independent software or by a formal proof.

Landmarks of computer-assisted mathematics

In 1976 Kenneth Appel and Wolfgang Haken proved the four-colour theorem by reducing it to checking that a set of 1,936 configurations, later reduced to 1,476, are each reducible, a task needing about 1,200 hours of computer time. The proof was controversial because no human could check the computation. A simplified proof by Robertson, Sanders, Seymour and Thomas in 1997 used 633 configurations, and in 2005 Georges Gonthier completed a fully formal proof in the Coq proof assistant, removing reasonable doubt.

In 1998 Thomas Hales, with Samuel Ferguson, announced a proof of the Kepler conjecture that no packing of equal spheres is denser than the familiar cannonball stacking, with density \(\pi/\sqrt{18} \approx 0.7405\). The proof involved solving about 100,000 linear programming problems. The referees reported that they were almost but not completely certain of its correctness, and the unease led Hales to launch the Flyspeck project, which completed a formal verification in 2014. In 2016 Marijn Heule, Oliver Kullmann and Victor Marek settled the Boolean Pythagorean triples problem: the integers 1 to 7,824 can be split into two classes with no class containing a Pythagorean triple \(a^2 + b^2 = c^2\), but 1 to 7,825 cannot. The proof was a satisfiability computation whose certificate occupied about 200 terabytes, checked by independent verified software.

Computation also discovers. In 1995 David Bailey, Peter Borwein and Simon Plouffe found, by an integer relation search using the PSLQ algorithm of Helaman Ferguson, the formula

which allows the hexadecimal digits of \(\pi\) to be computed individually without computing the earlier ones. The formula was found by computer and then proved by hand; its proof is a short exercise in integration once the formula is known. This pattern, computational discovery followed by conventional proof, is the ideal of experimental mathematics.

Exact versus floating-point arithmetic

The first rule of verification is to know what kind of numbers your computer is using. Floating-point numbers have about sixteen significant decimal digits, and arithmetic on them rounds at every step. For many purposes this is fine, but it is fatal for questions of exact equality, divisibility or sign when values are close to zero. Python's integers are exact and unbounded, and its fractions module provides exact rational arithmetic; use these whenever the question is exact.

from fractions import Fraction

# floating point: 0.1 cannot be represented exactly
total = 0.0
for _ in range(10):
    total += 0.1
print(total == 1.0, total, 0.1 + 0.2 == 0.3)
print(sum([Fraction(1, 10)] * 10) == 1)

# the order of summation changes a floating-point result
def add_up(xs):
    s = 0.0
    for x in xs:
        s += x
    return s
terms = [1 / k for k in range(1, 10 ** 6 + 1)]
forward, backward = add_up(terms), add_up(reversed(terms))
print(f"harmonic sum forward  {forward!r}")
print(f"harmonic sum backward {backward!r}")
print("difference:", forward - backward)

# an exact question asked in floating point: is (1e16 + 1) - 1e16 equal to 1?
print((1e16 + 1) - 1e16, (10 ** 16 + 1) - 10 ** 16)

False 0.9999999999999999 False
True
harmonic sum forward  14.392726722864989
harmonic sum backward 14.392726722865772
difference: -7.833733661755105e-13
0.0 1

Adding 0.1 ten times does not give exactly 1, and \(0.1 + 0.2\) is not exactly \(0.3\). The two harmonic sums differ in the last digits because rounding errors accumulate differently, and adding \(1\) to \(10^{16}\) in floating point is lost entirely. Since version 3.12, Python's built-in sum function uses a compensated summation algorithm that largely hides the first two effects, which is why the program accumulates in an explicit loop, as most numerical code in other languages does. Neither effect matters for a plot; both matter for a claim of equality. When floating point is unavoidable, as in numerical integration, report results with a justified error bound, or use interval arithmetic, which tracks guaranteed bounds on every quantity.

A worked case: Egyptian fractions

Ancient Egyptian scribes wrote fractions as sums of distinct unit fractions, such as \(\frac{2}{5} = \frac{1}{3} + \frac{1}{15}\). In 1202 Fibonacci described a greedy method: subtract the largest unit fraction not exceeding the remainder, and repeat. James Joseph Sylvester proved in 1880 that this always terminates. The proof is a model of how a simple invariant settles a question that computation alone could only suggest.

Theorem. For every rational number \(0 < \frac{p}{q} < 1\) in lowest terms, the greedy algorithm produces a finite sum of distinct unit fractions equal to \(\frac{p}{q}\).

Proof. Let \(n = \lceil q/p \rceil\), the smallest integer with \(\frac{1}{n} \le \frac{p}{q}\). Then \(n - 1 < q/p\), so \(p(n - 1) < q\), that is \(pn - q < p\). The remainder is

whose numerator \(pn - q\) satisfies \(0 \le pn - q < p\). If it is 0 we are done. Otherwise the remainder, in lowest terms, has numerator at most \(pn - q\), which is strictly less than \(p\). The numerators therefore form a strictly decreasing sequence of positive integers, which must reach 0 after at most \(p\) steps. The unit fractions are distinct because each remainder is less than the unit fraction just subtracted: from \(\frac{p}{q} < \frac{1}{n - 1}\) we get \(\frac{p}{q} - \frac{1}{n} < \frac{1}{n - 1} - \frac{1}{n} = \frac{1}{n(n - 1)} \le \frac{1}{n}\), so the next denominator exceeds \(n\). \(\blacksquare\)

The proof bounds the number of terms by the numerator, but says nothing about the size of the denominators, which can be enormous. Here computation is the right tool, and it should use exact arithmetic.

from fractions import Fraction
from math import ceil

def greedy(x):
    """greedy Egyptian fraction expansion of a rational 0 < x < 1"""
    parts = []
    while x > 0:
        n = ceil(Fraction(x.denominator, x.numerator))
        parts.append(n)
        x -= Fraction(1, n)
    return parts

for p, q in [(2, 5), (4, 13), (5, 121), (7, 15), (3, 7)]:
    d = greedy(Fraction(p, q))
    assert sum(Fraction(1, n) for n in d) == Fraction(p, q)       # exact check
    print(f"{p}/{q} = " + " + ".join(f"1/{n}" for n in d))

# 5/121: the greedy method is short in terms but huge in size
d = greedy(Fraction(5, 121))
print("largest denominator for 5/121 has", len(str(d[-1])), "digits")
# numerators of the remainders strictly decrease, as the proof says
x, nums = Fraction(5, 121), []
while x:
    nums.append(x.numerator)
    x -= Fraction(1, ceil(Fraction(x.denominator, x.numerator)))
print("numerators:", nums)

2/5 = 1/3 + 1/15
4/13 = 1/4 + 1/18 + 1/468
5/121 = 1/25 + 1/757 + 1/763309 + 1/873960180913 + 1/1527612795642093418846225
7/15 = 1/3 + 1/8 + 1/120
3/7 = 1/3 + 1/11 + 1/231
largest denominator for 5/121 has 25 digits
numerators: [5, 4, 3, 2, 1]

The expansion of \(\frac{5}{121}\) has only five terms, as the proof guarantees at most five, but its last denominator has 25 digits, although \(\frac{5}{121} = \frac{1}{33} + \frac{1}{121} + \frac{1}{363}\) shows that a short expansion with small denominators exists. The greedy algorithm is correct but not optimal, and the gap between correctness and optimality is a rich source of project questions. The Erdős–Straus conjecture, that \(\frac{4}{n} = \frac{1}{x} + \frac{1}{y} + \frac{1}{z}\) has a solution in positive integers for every \(n \ge 2\), has been verified by computer for all \(n\) up to very large bounds but remains open, and is a classic example of an experimental project topic.

Making computations trustworthy

A computation that supports a claim in your thesis should meet several standards.

Test on known cases. Before trusting a program on new inputs, run it on inputs where you know the answer: small cases computed by hand, values from the literature, special cases with closed forms.

Check independently. Compute the same quantity two different ways, as Amara did when she generated representations directly and compared them with a divisor sieve. Agreement of two independent methods is far more convincing than either alone.

Prefer certificates. Some answers are hard to find but easy to check. A factorization of a large number, a solution of an equation, a colouring of a graph or a satisfying assignment of a formula can be verified quickly however it was found. When your computation produces such an object, record it and verify it separately. The 200-terabyte Pythagorean triples proof was trusted because its certificate was checked by an independently verified program.

Make it reproducible. Record the code, the versions of the software, the random seeds and the running time. Every number in the thesis should be regenerable by running a script, and the scripts should be included in an appendix or a public repository.

def sieve(n):
    is_p = bytearray([1]) * (n + 1)
    is_p[0:2] = b'\x00\x00'
    for p in range(2, int(n ** 0.5) + 1):
        if is_p[p]:
            is_p[p * p::p] = bytearray(len(is_p[p * p::p]))
    return is_p

N = 200000
P = sieve(N)
primes = [p for p in range(N + 1) if P[p]]

# Goldbach: every even n in 4..N is a sum of two primes; record a certificate for each n
cert = {}
for n in range(4, N + 1, 2):
    for p in primes:
        if P[n - p]:
            cert[n] = (p, n - p)
            break
missing = [n for n in range(4, N + 1, 2) if n not in cert]

# check the certificates independently of the search, by trial division
def is_prime(m):
    return m >= 2 and all(m % d for d in range(2, int(m ** 0.5) + 1))
sample = list(cert.items())[::997]
print("even numbers without a decomposition:", missing)
print("independently rechecked certificates:", all(is_prime(a) and is_prime(b) and a + b == n for n, (a, b) in sample), f"({len(sample)} sampled)")
worst = max(cert, key=lambda n: cert[n][0])
print("largest smallest prime needed:", cert[worst][0], "for n =", worst)

even numbers without a decomposition: []
independently rechecked certificates: True (101 sampled)
largest smallest prime needed: 383 for n = 194470

The Goldbach conjecture has been verified for all even numbers up to \(4 \times 10^{18}\) by Tomás Oliveira e Silva, Siegfried Herzog and Silvio Pardi, using exactly this structure on a vastly larger scale: an efficient search, a certificate for each case, and careful checking. The observation that the smallest prime needed stays tiny, as the program shows, is itself a heuristic reason to believe the conjecture.

Computer algebra and specialized software

Beyond general-purpose languages, research mathematicians use computer algebra systems such as SageMath, Mathematica, Maple and Magma for symbolic computation; GAP for group theory; PARI/GP for number theory; SnapPy for low-dimensional topology; SAT and SMT solvers for combinatorial search; and integer relation algorithms such as PSLQ for discovering identities. Learn whichever is standard in your project's area, ideally guided by your supervisor. Cite the software you use, with version numbers: it is part of your method, and zbMATH's swMATH service indexes mathematical software and the papers that use it.

AI systems in mathematical research

The years 2024 to 2026 brought rapid change. In July 2024 Google DeepMind's AlphaProof and AlphaGeometry 2 together reached silver-medal standard on the International Mathematical Olympiad problems, working in the Lean proof language. In July 2025 both an advanced version of Google's Gemini with Deep Think and an experimental OpenAI model achieved gold-medal scores, 35 out of 42, writing natural-language proofs within the contest time limits. Large language models are now used routinely to explain papers, suggest approaches, write code and draft text, and systems coupled to proof assistants have formalized substantial bodies of mathematics, as lesson 8 describes.

For an honours student these tools are powerful and hazardous in equal measure. They can be confidently wrong: they can produce a fluent proof with a fatal gap, a computation with an arithmetic error, or a reference that does not exist. They can also short-circuit the learning that the project exists to produce. Sensible practice is to treat AI output exactly as you would treat an unrefereed preprint by an unknown author: as a source of ideas to be checked, never as an authority. Verify every claim yourself, by proof, by independent computation or against the actual literature. Follow your department's policy and disclose substantial use in the thesis. The examiners will assess your understanding at the oral examination, and no tool can supply that.