Automatically generating combinatorial conjectures It very often happens that one reduces a problem to a bunch of combinatorial data, and need to sift through this data for patterns, which form conjectures on which to do "real" mathematics. Problems of this sort are why the OEIS exists; however, it doesn't enumerate every arithmetical rule, not even all of those $\mathbb{N} \to \mathbb{N}$.
This seems like a problem that's eminently solvable algorithmically―but, before I went iterating through numberings of primitive-recursive functions, I wanted to ask if there's a canonical solution. Is the naïve Boolean satisfiability approach (one constraint for each data point) more sensible? Stuff I'm not thinking about?
For clarity, what I'm looking for is a way to search through the set of (computable) functions $\mathbb{N} \times \cdots \times \mathbb{N} \to \mathbb{N}$ for the simplest nontrivial algorithm consistent with a list of input-output pairs.
 A: Perhaps, the most significant (and first?!) example of such automatically generated combinatorial conjectures was Graffiti created by Siemion Fajtlowicz in 1982/3 or so. Later, he was joined by his student Ermelinda DeLaViña;
see:

*

*https://web.archive.org/web/20090302092953/https://www.math.uh.edu/~clarson/graffiti.html

*https://en.wikipedia.org/wiki/Graffiti_(program).

Paul Erdos and other mathematicians enjoyed Graffiti.
A: While this may not be exactly what you asked for, it seems close. Thibault Gauthier, Miroslav Olšák, and Josef Urban posted an arXiv preprint (apparently on the same day you posted your question here on MO!), Alien Coding, arXiv:2301.11479. Here is the abstract:

We introduce a self-learning algorithm for synthesizing programs for OEIS sequences. The algorithm starts from scratch initially generating programs at random. Then it runs many iterations of a self-learning loop that interleaves (i) training neural machine translation to learn the correspondence between sequences and the programs discovered so far, and (ii) proposing many new programs for each OEIS sequence by the trained neural machine translator. The algorithm discovers on its own programs for more than 78000 OEIS sequences, sometimes developing unusual programming methods. We analyze its behavior and the invented programs in several experiments.

A: Looking into the SAT-solver idea, I noticed many modern solvers have systems for "syntax-guided synthesis:" given a grammar of acceptable primitives, search for a function implemented using those primitives that satisfies some logical specification.
Keep the mathematical ideas coming, but something of this nature with Racket's  Rosette is probably what I'm going to pursue for now.
A: Not sure whether this is exactly what you are looking for or whether you may consider this solution kind of cheating, but you may be interested in the Berlekamp–Massey algorithm, that can be used to find a shortest linear recurrence that generates a given sequence.
