// alien
ALIEN
An RL environment where agents assemble non-halting proofs for Turing machines.
// in plain terms
Some computer programs run forever, and proving that a specific one never halts can be extraordinarily hard. We built a training environment where an AI agent learns to assemble such proofs piece by piece, aimed at machines connected to famous unsolved problems. No such environment existed before.
// 01
Problem
A program's non-halting can be certified by exhibiting a finite automaton with the right closure properties. Constructing that automaton is the hard part, and no RL environment for building one existed. We built one: referee, environment, and a seed database of 88.7 million Turing machines.
// 02
Environment and referee
AGENT
proposes one transition
REFEREE
machine-checks it
CERTIFICATE
grows
The agent lays down the automaton one transition at a time, and a machine-checkable referee verifies every certificate. In the course of building it we found and reported a soundness bug in the reference Rust verifier. When the proposer is an adversarial learner, the referee has to be airtight.
// 03
Gate results
- +The v1 pre-registered gate failed: the shaped reward carried no information beyond the win bit. The failure is reported in full.
- +Reworked to survival-depth fitness: reward correlation with distance-to-solution rose from ~0.05 to 0.62–0.64, and the environment ran 13.7× faster.
- +The v3 gate passed on 1,300 fresh machines: evolutionary vs random solve-ratio 1.197 (p = 6×10⁻⁷), and 2.80× on the hardest frontier stratum.
// 04
Next steps
BB(5) — solved world
BB(6) — 1,016-machine leaderboard
RH MACHINE — 744 states
the benchmark ladder — each rung harder than everything below it
The AlphaZero-style self-play stack is built and verified, waiting on GPU time. The bar to beat is 274/300 overall and 70/83 on the frontier. Above that, the ladder climbs from the solved BB(5) world through the BB(6) leaderboard toward the 744-state machine whose non-halting is equivalent to the Riemann Hypothesis.
// the thread
Status
The self-play stack is built and verified but untrained: a promising environment with an unproven agent. Whether a learned policy beats the evolutionary arm is the open question. If it does, an agent will be writing small non-halting proofs no one taught it. If it does not, we will report that result as well.