aidan yu
← back to projects

first light

I wanted to see whether a search program could rediscover a piece of mathematics without being told the answer. FIRST LIGHT starts with the real numbers, proposes new ways to multiply, and checks which ones actually work.

role
Search system for exploring which mathematical ideas are worth trying next.
language
Python. The main checker uses exact int64 arithmetic; Z3 and SymPy are used for supporting analysis.
scale
About 65 billion proposals and 30.7 billion screened candidates.
status
Experiment complete. Private repository.

The experiment

I chose the normed division algebras as the target. Roughly speaking, these are number systems where addition, subtraction, multiplication, and division work, and where multiplying two numbers also multiplies their lengths. The real numbers are one example. The complex numbers, quaternions, and octonions are the other three.

Hurwitz proved in 1898 that the list ends there. That gives the experiment a convenient answer key: dimensions 1, 2, 4, and 8 work; dimensions 3 and 16 do not. Finding the familiar examples was only half the test. The search also had to come up empty in the right places.

FIRST LIGHT found valid structures in dimensions 1, 2, 4, and 8, and none in dimensions 3 and 16. Results by dimension dim 1 ℝ given base world dim 2 ℂ found 1 of 25 dim 3 × none found 0 of 244,672,066 dim 4 ℍ found 6 of 6 walkers dim 8 𝕆 found 4 of 60 dim 16 × none found 0 of 4 Hurwitz (1898): normed division algebras exist only in dimensions 1, 2, 4, and 8.
Figure 1. What the search found. Dimension 1 was the starting point. The same procedure then found valid structures in dimensions 2, 4, and 8. It found none in dimensions 3 or 16, matching Hurwitz's theorem.

How candidates are checked

The program has two separate parts. A search process proposes multiplication tables, then a fixed checker returns pass or fail. There is no model inside the checker and no score to negotiate: a candidate either satisfies the required identities or it does not.

Keeping those parts separate turned out to matter. In two exploratory runs, the search learned to score well without getting any closer to a division algebra. All 123,000 of those proposals still failed the final check. Every candidate that passed was then checked again by a second implementation that shares no code with the first.

Candidates move from search through screening, an exact checker, and an independent second check. How a candidate is checked proposals ~65 × 10⁹ screen 30.7 × 10⁹ exact checker int64, exact second check independent code path accepted result rejected the checker imports only: itertools · numpy · dataclasses no floats, model, or proof assistant
Figure 2. The checking pipeline. Cheap screens discard most proposals before they reach the exact checker. A separate implementation checks every result again, which makes it less likely that one bug can create a false positive.

Getting to eight dimensions

A direct search in dimension 8 went nowhere, so I changed the approach. I fit a general doubling rule using only the structures already found in dimensions 1, 2, and 4. That produced 60 possible rules. I saved the complete list before running anything in dimension 8, applied each rule once, and four of them worked.

There were two nice surprises. The result satisfied Degen's eight-square identity, and it was alternative, a characteristic property of the octonions that the search was never rewarded for producing. That made the result more convincing than simply passing the test I had written.

Run totals: about 65 billion proposals, 30.7 billion screened candidates, and 60 million operator evaluations.

The script that builds the figures reads these counts directly from the saved run files.

Notes from the experiment

The dimension 3 search was not one uniform exhaustive test. One family had 531,441 members, all checked exactly on the CPU. The other had 244 million and was screened on the GPU in float32 using a recorded analytic error bound. Neither family reached the acceptance threshold, but they were checked in different ways.

I did not use a proof assistant for this project. In my notes, “kernel check” means a small decision procedure—an exhaustive sweep, exact fixpoint, or SMT query—not a Lean, Coq, or Isabelle proof.

FIRST LIGHT also began with a different idea: train a foundation model from scratch for this job. I scored that version 1.5 to 2 out of 10 against the criteria I set beforehand and dropped it. The search-and-check system described here is what survived.