Quickstart

Get started in just a few lines: load a dataset, define hypotheses, and generate mathematical conjectures using symbolic expressions and heuristics.

Step 1: Load your data

You can use any pandas.DataFrame—TxGraffiti works on tabular data with numeric or boolean columns.

Try the built-in graph dataset:

from txgraffiti.example_data import graph_data
df = graph_data  # structured invariants for connected graphs

Step 2: Initialize a playground

Wrap your dataset in a ConjecturePlayground session. This gives you symbolic access to all features.

from txgraffiti.playground import ConjecturePlayground

ai = ConjecturePlayground(
    df,
    object_symbol="G",      # used in printed formulas (∀ G: …)
    base="connected",       # optional: global assumption
)

Step 3: Define hypotheses

You can build logical predicates using symbolic expressions:

regular = ai.max_degree == ai.min_degree
cubic   = regular & (ai.max_degree == 3)
small   = ai.max_degree <= 3
not_complete = ~ai.Kn

Step 4: Generate conjectures

Choose your generator methods, features, target invariant, and heuristics:

from txgraffiti.generators import ratios, convex_hull, linear_programming
from txgraffiti.heuristics import dalmatian_accept, morgan_accept
from txgraffiti.processing import remove_duplicates, sort_by_touch_count

ai.discover(
    methods         = [ratios, convex_hull, linear_programming],
    features        = [ai.independence_number],
    target          = ai.zero_forcing_number,
    hypothesis      = [cubic, small & not_complete],
    heuristics      = [dalmatian_accept, morgan_accept],
    post_processors = [remove_duplicates, sort_by_touch_count],
)

Step 5: Print your top conjectures

for i, conj in enumerate(ai.conjectures[:5], start=1):
    print(f"Conjecture {i}.", ai.forall(conj))
    print("    Accuracy:", f"{conj.accuracy(df):.0%}\n")

Example output:

Conjecture 1. ∀ G: ((connected) ∧ (regular) ∧ (max_degree == 3)) → (zero_forcing_number ≥ 3)
    Accuracy: 100%

Conjecture 2. ∀ G: ((connected) ∧ (max_degree ≤ 3) ∧ (¬(Kn))) → (zero_forcing_number ≤ (1 + independence_number))
    Accuracy: 100%

Conjecture 3. ∀ G: ((connected) ∧ (regular) ∧ (max_degree == 3)) → (zero_forcing_number ≥ ((2 · independence_number) − 8))
    Accuracy: 100%

Conjecture 4. ∀ G: ((connected) ∧ (max_degree ≤ 3) ∧ (¬(Kn))) → (zero_forcing_number ≥ ((6/5 · independence_number) − 37/5))
    Accuracy: 100%

Conjecture 5. ∀ G: ((connected) ∧ (max_degree ≤ 3) ∧ (¬(Kn))) → (zero_forcing_number ≤ ((−1/5 · independence_number) + 47/5))
    Accuracy: 100%

What’s next?

Try other generators like in_reverie or make_upper_linear_conjecture.
Swap in your own dataset of tabular numerical data.
Explore how to export formulas to Lean 4 or generate new predicates recursively.