Self-replicating programs appear on their own in a soup of random code. Testing one on a few thousand partners is evidence. We wanted certainty, so we asked Lean to check, for every one of the 25664 possible partners, which of them really copy themselves, and to certify the exact collision where life began in one world.
The two programs are glued into one 128-byte tape and run, exactly as the soup did it. Watch the right half.
Instead of trying partners one by one, run the program once against a partner whose 64 bytes are all unknown (?). A byte becomes known only when the program writes it. If the run never has to look at an unknown byte to decide what to do next, its outcome is the same for all 25664 partners. Lean’s kernel replays exactly this run, all 8,192 steps, and a separate proof shows the shortcut is sound.
The theorems are about a Lean transcription of BFF, cross-checked against our Python and C interpreters on 240 test tapes. Each certificate is one kernel computation per organism plus a soundness proof shared by all of them.