Graffiti3 : Compact Theory Libraries for Automated Mathematical Discovery

We study automated conjecturing: the computer-assisted generation of human-readable symbolic statements intended for expert inspection and subsequent proof or refutation. We formalize conjecture generation as theory selection over a finite, evolving evidence base represented by a streaming invariant table, whose rows (objects) and columns (invariants, predicates, and derived features) expand as new constructions and counterexamples are discovered. We present Graffiti3 , a domain-agnostic engine that converts such tables into a compact theory library: a budgeted, nonredundant set of snapshot-true bounds, implications, and structural annotations drawn from a controlled grammar. Candidate statements are produced by optimization and then filtered and ranked by explicit simplicity criteria together with dominance-style redundancy elimination, yielding a small library designed for iterative questioning, counterexample search, and downstream deductive work. To support such reasoning, Graffiti3 augments conjectures with short sufficient conditions that explain equality and near-equality regimes, exhaustively verifies each output in the current snapshot, and treats conjectures as provisional until they survive targeted counterexample search or are proved. We also describe a hybrid workflow in which a large language model proposes derived features and narrative summaries while Graffiti3 provides deterministic validation and theory selection. In integer arithmetic, we prove two conjectures produced by this workflow, yielding characterizations of squarefree integers. We demonstrate the methodology on finite groups, knot theory, and a Calabi–Yau hypersurface census, and we revisit graph-theoretic conjectures from the predecessor system TxGraffiti, recalling open problems and reporting new ones.