Autonomous formal verification of Initio's proof of Ehrhart's Volume Conjecture

In a previous post, we shared an alternative proof of Ehrhart’s Volume Conjecture, obtained independently and using models available for public use.

We’re sharing here a formal verification of the result, also autonomously generated, along with a document describing the formalized proof. Interestingly, the process of formalization found ways to streamline Initio’s algebraic proof strategy. While the core idea is still the same, some intermediate constructions and arguments are presented more cleanly.

This validates the autonomously obtained result. Beyond the verification, having two substantially different proofs of the same result may point to interesting mathematical relationships between the proof techniques.

A document with more details of the verified proof is available here.

The code is available here.