I’d really love to know if anyone knows of literature on generating examples in mathematically robust ways. It’s hard to search for literature on this because of how Google interprets the query. I know there’s work here in formal language theory, as it’s usually straightforward to generate a sentence given a formal grammar. But I really want to know what work has been done in a more general context of mathematical structures. Questions like ” what is the simplest example of structure X” or “smallest example that can be differentiated from the others” or “simplest counter-example”. I know there’s work on example-driven programming and the like, which I assume would have some relevance, but I’ve had no luck finding much. I just have to assume that this is a question that some mathematicians somewhere have asked before.

is this for testing? you might find a something with quickcheck or its related research.

Not for testing, looking for theoretical work as the question is relevant to my current research. QuickCheck might be what I saw before! I’ll check it out.

This reminds me of Barliman

Besides Quickcheck, I thought of model-checking software like Z3 (very easy to play with in Python!), Alloy, MiniZinc, maybe even TLA+. I haven't used the latter three (which are not an exhaustive list either), but they seem to be very powerful.

I would add Lean4 to the counter-example-finding list.

This seems relevant: https://hackage.haskell.org/package/smallcheck

"Property-based testing" is the more general keyword to search for. QuickCheck is its best-known implementation, but theoretical work doesn't necessarily refer to it.

Hopefully ‘property-based testing’ can help me find relevant research. It still seems slightly off what I’m looking for, but it’s closer. I’m less interested in programming languages here, and hoping there’s some more general mathematical work along these lines. I’d love to have a framework to talk about things like “a tree with a branching factor of 5”, “a partially ordered set”, “a directed graph containing a subgraph that is equivalent to a binary tree” and to talk about these general kinds of structures and properties with some formal notion(s) of “examples”.

It sounds to me like you want to use a model-checker too. If you give one a program and a condition, they're designed to give you example states the program can get into that satisfy the condition, but they're more general than that. If you input a model that describes graphs generally, and encode a condition that corresponds to "branching factor of 5" then a model-checker will give you an example of such a graph. Many examples, if you ask for them!

Something else that might be useful is L-systems (https://en.wikipedia.org/wiki/L-system), used mainly for simulating plant growth.

Also quickspec and symbolic execution come to mind as relevant (https://hackage.haskell.org/package/quickspec-2.1.5/docs/QuickSpec.html)

I didn't know QuickSpec, which looks very relevant, thanks!