Lower Bounds for Multivariate Independence Polynomials
The multivariate independence polynomial is the partition function of the hard-core model with per-vertex fugacities. The paper proves a lower bound extending to the multivariate setting a result Tao proved in the univariate case, and settles a conjectured generalization for a multiaffine version of the semiproper colouring partition function with two proper colours.
- Result
- Proved
- Status
- Resolved
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Extremal combinatorics; statistical physics
- Posed by
- —
- Year posed
- —
- Years open
- —
- Solved
- 2026-08-05
- Model
- Aletheia (Gemini Deep Think), Harmonic Aristotle
- Vendor
- Google DeepMind, Harmonic
- Collaborators
- Joonkyung Lee, Jaehyeon Seo
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 12 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
"The key steps in both proofs were obtained, at least in part, by using Aletheia, a mathematics research agent built upon Gemini Deep Think at Google DeepMind." The paper marks where the agent contributed, publishes raw prompts and outputs in a repository, and calls the work a benchmark demonstrating that current models can in part assist with mathematical research. Theorem 1.4 was separately formalized in Lean 4 with Harmonic Aristotle.
Verification
Theorem 1.4 is formalized in Lean 4 using Harmonic Aristotle, with the files public; the rest of the paper is not formalized, and nobody independent has audited the informal-to-formal correspondence.