txgraffiti.export_utils package

Submodules

txgraffiti.export_utils.lean4 module

Module for exporting TxGraffiti conjectures to Lean 4 syntax.

This module converts symbolic TxGraffiti Conjecture objects into Lean-compatible theorems. It keeps hypotheses in Prop/ℕ (adding connected G and order G ≥ (2 : ℕ) if missing), and makes the conclusion type-correct by casting fractions to ℚ, typing all remaining integers, and coercing invariants to a single ambient type in the conclusion.

txgraffiti.export_utils.lean4.auto_var_map(df, *, skip=('name',))[source]

Return {column -> ‘col G’} for Lean-friendly substitution.

Return type:

dict[str, str]

txgraffiti.export_utils.lean4.conjecture_to_lean4(conj, name, *, object_symbol='G', object_decl='SimpleGraph V')[source]
Return type:

str

Build a Lean theorem skeleton:
theorem <name> (GSimpleGraph V)

(h1 : P1 G) (h2 : P2 G) … : <raw-conclusion> :=

sorry

txgraffiti.export_utils.lean4.conjectures_to_lean(conjs, *, name_prefix='Conj')[source]
Return type:

List[str]

Convert repr strings like

“<Conj (chordal) → (independence_number >= 5)>” “<Conj (tree) → (independence_number = 2 + residue)>” “<Conj (planar) → (independence_number <= (-1/2 * total_domination_number) + 7)>” “<Conj (subcubic) → (7 + residue <= independence_number)>”

into Lean theorems with standard hypotheses and clean types.

Pipeline per conjecture:

  1. Parse hypothesis ‘prop’ and inequality ‘lhs op rhs’.

  2. If the invariant is on the RHS and not on LHS, swap sides and flip op.

  3. Parse RHS as a linear combination over allowed invariants with a rational constant.

  4. Determine a common α ∈ {ℕ, ℤ, ℚ, ℝ} via the type join of LHS and all RHS vars.

  5. Multiply both sides by positive integer L = lcm(denominators) to clear fractions.

  6. Normalize signs: move all negative RHS terms (including negative constant) to LHS. After this step, the RHS has only nonnegative coefficients (and possibly 0).

  7. Render both sides in Lean with casts to α, preserving the original inequality operator.

Note

  • Because we only add the same nonnegative expression to both sides in step (6), the inequality direction is preserved (no flipping after normalization).

  • When α = ℕ, RHS being a sum of nonnegative terms avoids writing negative naturals.

txgraffiti.export_utils.lean4.necessary_conjecture_to_lean(conjectures, func_names, *, name_prefix='TxGraffitiBench')[source]

Render a batch of necessary conjectures (hypothesis ⇒ numeric inequality) into Lean theorems, fully typed.

Parameters:

  • conjectures (list[Conjecture]) – TxGraffiti conjectures whose conclusions are `Inequality`s.

  • func_names (iterable[str]) – Names of invariants/properties that must appear as ‘<fn> G’ in Lean. e.g., [“independence_number”,”matching_number”,”zero_forcing_number”,…]

  • name_prefix (str) – Prefix for theorem names (theorems are numbered 1..n).

Returns:

list[str]

Return type:

Lean theorems with typed conclusions.

Module contents