Automatic Proofs for Formulae Enumerating Proper Polycubes

We develop a general framework for computing formulae enumerating polycubes of size n which are proper in n−k dimensions (spanning all n−k dimensions), for a fixed value of k. Besides the fundamental importance of knowing the number of these simple combinatorial objects, such formulae are central in the literature of statistical physics in the study of percolation processes and the collapse of branched polymers. We re-affirm the already-proven formulae for k≤3, and prove rigorously, for the first time, that the number of polycubes of size n that are proper in n−4 dimensions is 2n−7nn−9(n−4)(8n8−128n7+828n6−2930n5+7404n4−17523n3+41527n2−114302n+204960)/6.