A Generalization of Boppana's Entropy Inequality
A generalization of Boppana's entropy inequality, of the kind used in union-closed-sets arguments, proved and formalized: the sharp form with the extremal constant characterized via the unique positive solution of an explicit equation.
- Result
- Proved
- Status
- Resolved
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Entropy inequalities
- Posed by
- —
- Year posed
- —
- Years open
- —
- Solved
- 2026-01-27
- Model
- GPT-5.2 Pro, Harmonic Aristotle, Gemini 3 Pro
- Vendor
- OpenAI, Harmonic, Google DeepMind
- Collaborators
- Boon Suan Ho
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 8 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
"Key steps in some proofs were generated with the assistance of GPT-5.2 pro. The result has also been formalized in Lean 4 using Harmonic Aristotle and Gemini 3 Pro Preview" - with the formalization public.
Verification
Formalized in Lean 4 (Aristotle plus Gemini); code public on GitHub. No independent review. Tier: the formalization was produced by the assisting systems and checked by the author; no independent statement audit.