Proof of Life
Computational Life · Lean 4

Proof of Life.

In a soup of 131,072 random programs, two programs that cannot copy themselves collide, with no mutation. One of the pieces that comes out copies itself, backwards, into every one of the 25664 possible partners. We reconstructed that collision byte for byte and proved it in Lean.

1 birthcertified: the exact collision where life began in world 52, epoch 5,858
22 of 25organisms under the paper’s rules proved to copy themselves for every partner (7 of 28 under the other head rule)
99.99%of 24 million copy steps in living soups run backwards, so every species lives as two mirror strands
theorem birth_certificate_world52 : run (A ++ B) = A_out ++ C ∧ (∀ X : Vector UInt8 64, run (C ++ X) = C ++ C.reverse) ∧ …