Given some initial list of assumptions, I'd like to generate some true statements which follow from them without seeking a specific proof goal. I only need a small number of consequences from those assumptions, so there's no need to find every possible consequence.
Is there any proof assistant (or ATP) which has this functionality? And if not, is there some tactic or strategy within an assistant which I could modify to produce this result?
This definitely falls under various active research projects to find interesting mathematics from a set of theorems. I can't point to a particular project per say, but let me mention why this is so hard.
The main reason it is so hard is that any naive algorithm which just starts combining statements is going to get into a combinatorial explosion of uninteresting mathematics.
For example, if my initial statements are A, B, C then I can form all sorts of things like A /\ B, A -> B, true, not not B.
Moreover if I have forall n m : Nat, n + m = m + n, then I can form 1 + 2 = 2 + 1, (1+1)*3 + 4 = 4 + (1+1)*3 and forall n m : Nat, n + 0 = 0 + n.
If I have A and A -> B, then I can form B, but often I really have A and A' -> B where A' doesn't exactly match A, so I first have to prove A' (or more likely if A' depends on a variable, I have to choose the right instance of that variable).
If I have forall a: A, f(a) = g(a), and I have some statement B about f(a), then I can rewrite any of the occurrences of f(a) in B, but it is hard to know which rewrites are interesting or useful for further downstream combinations.
I'm sure there is some work going back to the early days of AI of trying to just randomly mix axioms to get new math. And I imagine they used a lot of heuristics (probably to mixed success). I however, don't know any references.
Also, in FOL, resolution theorem provers first make all formulas into CNF so in the end you just have a list of disjunctive clauses. It is clear then what it means to combine two clauses. Indeed, an automatic theorem prover takes a bunch of clauses it wants to show are mutually inconsistent and just combines clauses using some heuristics until it reaches a proof of false. This cuts down on some redundancy, but there is still combinatorial explosion, and better heuristics can make huge gains in efficiency of ATPs.
If your goal is to create problems for say training an AI, then look at my answer to What are some automated theorem generators? What background logic do they use and what heuristics do they use for theorem-goodness?.
And in general in AI for mathematics research there is always the question (with IMO no good answers so far) of can we program or train a computer to determine what "interesting" mathematics looks like?
1 = 1,2 = 2,3 = 3,4 = 4, ... etc? $\endgroup$