Playground

ConjecturePlayground is your main entry point for automated conjecture discovery. It wraps a pandas.DataFrame and provides methods to:

• Generate conjectures via multiple generators (convex_hull, ratios, lp_model, …)

• Filter them with heuristics (morgan, dalmatian, …)

• Post‐process (sort, dedupe, strengthen equalities)

• Quantify them (forall, exists)

• Persist new hypotheses (discover_equalities)

• Export results to JSON/CSV or Lean theorem stubs

Class Signature

class ConjecturePlayground:
    def __init__(
        self,
        df: pandas.DataFrame,
        object_symbol: str = "G",
        *,
        base: Optional[Union[str, Predicate]] = None
    ):
        ...

    def discover(
        self, *args, **kwargs
    ) -> List[Conjecture]:
        ...

    def generate(
        self, *,
        methods: Optional[List[Callable]] = None,
        features: Optional[List[Union[str,Property]]] = None,
        target: Optional[Union[str,Property]] = None,
        hypothesis: Optional[
            Union[str, Predicate, Sequence[Union[str,Predicate]]]
        ] = None,
        heuristics: Optional[List[Callable]] = None,
        post_processors: Optional[List[Union[str,Callable]]] = None,
        **kwargs
    ) -> Iterator[Conjecture]:
        ...

    def discover_equalities(
        self, *,
        generators: Optional[List[Callable]] = None,
        min_fraction: float = 0.15
    ) -> List[Predicate]:
        ...

    def append_row(self, row: dict) -> None: ...
    def reset(self, new_df: Optional[pd.DataFrame] = None) -> None: ...
    def export_conjectures(self, path: str, format: str = "json") -> None: ...
    def export_to_lean(
        self, path: str,
        name_prefix: str = "conjecture",
        object_symbol: Optional[str] = None
    ) -> None: ...
    def convert_columns(self, convert_dict: dict) -> None: ...

Initialization (__init__)

• df: the DataFrame to explore

• object_symbol: a name used by .forall/.exists in pretty printing

• base: an optional Predicate or column name to conjoin with every hypothesis (defaults to TRUE, i.e. no restriction)

Discovery (discover)

A one‐stop method that runs:

1. Generators (all registered or user‐supplied) × Hypotheses (base ∧ each given)

2. Heuristics in sequence (global kept list)

3. Post‐processors on the final list (e.g. remove_duplicates, sort_by_touch_count)

Returns the full list of accepted Conjecture objects and caches them in .conjectures.

Generation (generate)

The streaming equivalent of discover. Yields Conjecture objects one by one, in generator order, before any post‐processing. Signature mirrors discover but returns an iterator.

Quantifiers (forall, exists)

• pg.forall(pred) wraps a Predicate in universal notation (∀ G: …)

• pg.exists(pred) wraps in existential notation (∃ G: …)

Hypothesis Mining (discover_equalities)

Automatically finds any single-feature inequalities L ≤ R or L ≥ R (under TRUE) that are tight on at least min_fraction of the rows, registers them as new Predicate`s (`L_eq_R), and returns them sorted by support.

Dataframe Updates

• append_row(row: dict) adds a new row in place and invalidates the cache

• reset(new_df: DataFrame = None) replaces or rebinds the DataFrame, clearing cached conjectures

Exporting

• def conjecture_to_lean4(conj: Conjecture, name: str, object_symbol: str = “G”, object_decl: str = “SimpleGraph V”) -> str writes Lean 4 theorem stubs for all cached conjectures

Column Conversions

• convert_columns(convert_dict) applies a mapping function to existing columns, e.g. to preprocess raw values into Booleans or enums.

Illustrative Example

import pandas as pd
from txgraffiti.playground import ConjecturePlayground
from txgraffiti.generators import convex_hull, ratios, lp_model
from txgraffiti.heuristics import morgan, dalmatian
from txgraffiti.postprocessing import remove_duplicates, sort_by_touch_count

# 1) Load your DataFrame
df = pd.read_csv("graph_data.csv")

# 2) Create a playground with base hypothesis “connected”
pg = ConjecturePlayground(df, object_symbol="G", base="connected")

# 3) Auto-mine any equality hypotheses holding ≥20% of rows
new_hyps = pg.discover_equalities(min_fraction=0.2)

# 4) Run full discovery over two hypotheses:
conjs = pg.discover(
    methods         = [convex_hull, ratios, lp_model],
    features        = ['order','matching_number','min_degree'],
    target          = 'independence_number',
    hypothesis      = new_hyps,          # includes base ∧ each discovered
    heuristics      = [morgan, dalmatian],
    post_processors = [remove_duplicates, sort_by_touch_count],
    round_decimals  = 2,
    drop_coeff_below= 0.05,
)

# 5) Export to Lean
pg.conjecture_to_lean4(
 "graph_conjectures.lean",
 name="graph_conj",
 object_symbol: str = "G",
 object_decl: str = "SimpleGraph V",
 )

# 6) Wrap and print top 3
for i, conj in enumerate(pg.conjectures[:3], start=1):
    print(f"Conjecture {i}.", pg.forall(conj))