Smooth lattice 3-polytopes with seven facets have the integer decomposition property

A lattice polytope P has the integer decomposition property if, for every positive integer k, every lattice point of kP is a sum of k lattice points of P. Oda conjectured that every smooth lattice polytope has this property. We prove the conjecture for smooth lattice polytopes of dimension three with seven facets. Together with the known case of at most six facets, every smooth lattice 3-polytope with at most seven facets has the integer decomposition property. The proof combines three criteria on the normal fan, based on slicing and projection, with the classification of smooth projective toric threefolds of Picard number four; the finitely many certificates are checked in Lean 4. The archive contains the paper (PDF, LaTeX source in the style of The Electronic Journal of Combinatorics, arXiv tarball), the certificates of the 625 families of fans, independent checkers in C, C++, Julia and Python, and a Lean 4 project with Mathlib in which the kernel checks every certificate for every value of the parameters (no native_decide; axioms propext, Classical.choice and Quot.sound only). The reduction, the three criteria and the classification are proved by hand in the paper.