AI Proof WatchKeep up with AI contributions

Lower bounds for multivariate independence polynomials and their generalisations

Joonkyung Lee, Jaehyeon Seo

Lee and Seo prove a degreewise lower bound for the multivariate independence polynomial at nonnegative vertex weights and a two-proper-colour semiproper partition-function bound. The model-origin Lemma 2.1 and dual-set ideas are retained central steps; the equality characterization in their first theorem is outside the Lean target.

Sources for this record

What was already known

Sah, Sawhney, Stoner and Zhao proved the single-weight bound. The heterogeneous-weight and two-colour bounds were new; the wider antiferromagnetic homomorphism conjecture remains open.

AI involvement AI-centered

Aletheia supplied a key multiplicative inequality and substantive dual-set and reduction ideas. Joonkyung Lee and Jaehyeon Seo formulated the project, finished the proofs and explained the arguments.

The paper identifies model-origin Lemma 2.1 and substantive dual-set/reduction ideas as central retained steps, while humans finished the two arguments.

Importance Notable

Extends graph-polynomial lower bounds to heterogeneous weights and semiproper colourings.

Limitations

A Lean 4 formalization covers the two-colour inequality and its single-colour specialization, not the equality characterization or every application. The authors completed several arguments from model sketches.

Technical verification Formal (Lean 4 / Mathlib with Harmonic Aristotle assistance)

Theorem 1.4's inequality is reported formalized in Lean 4, and its μ=0 specialization yields the inequality of Theorem 1.1. This does not document machine checking of the equality characterization in Theorem 1.1 or the paper's other applications. The Lean project was not built here.

Formal checking

Lean proof of the two-colour lower inequality under nonnegative vertex weights; its zero-second-colour case yields the one-colour inequality.

Checker
Seo's Lean 4 formalization and Lean type checker
Scope
Theorem 1.4 two-colour semiproper lower inequality for all finite graphs and nonnegative vertex weights; Theorem 1.1 lower inequality by μ=0 specialization
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Full

Lee and Seo explain the maximum-degree vertex-deletion induction and the dual-set log-convexity/reduction route, including where they replaced model sketches with their own proofs.

Correction and publication history

2026-10-18 · publication

Extends graph-polynomial lower bounds to heterogeneous weights and semiproper colourings.

Read this published revision