ALIEN CODES AND THEIR AUTOMATED AND HUMAN EXPLANATIONS

Slides: https://josefurban.eu/slides/scml26oeis.pdf . Abstract: We have automatically discovered symbolic explanations for over one-third of the sequences in the Online Encyclopedia of Integer Sequences (OEIS). The talk will describe the neuro-symbolic system consisting of a positive feedback loop that starts from zero knowledge and iterates between guessing the explanations, their verification, and training of the guessing methods. Then I will describe several additions and experiments that led to the current set of solutions found in hundreds of iterations of the feedback loop. I will show some of the solutions discovered. This includes over 80 programs for primes developed as the system self-evolves. I will also discuss a related experiment in automatically proving equivalences of the discovered programs using the SMT solver Z3. Because induction is often needed in such proofs, this leads to another self-learning neuro-symbolic system that repeatedly tries to guess the right instances of induction for Z3. Finally, I will also show some of the recent human explanations of the programs, mostly done by Tom Hales.