Computer-assisted proof of Havel's conjecture on spanning trees of hypercubes for dimension five

Ivan Havel in 1984 published a conjecture claiming that an arbitrary tree of maximum degree at most three on 2ⁿ vertices is a spanning tree of the 𝑛-dimensional hypercube iff its bipartition classes are of the same size. Four decades have passed and the problem is still open; the statement has been verified with computer assistance for 𝑛 ≤ 4 while for larger dimensions its validity is known only for several special cases. This dataset provides a machine-verifiable proof of the validity of Havel's conjecture for dimension 𝑛 = 5 . The submitted files contain the following:
computed_solution – a file containing the proof of Havel's conjecture for dimension 5
program.zip – an archive containing the program used to compute this solution, along with its documentation, including a function that receives a tree on 2⁵ vertices satisfying the assumptions of the conjecture in graphwiz format and outputs the desired embedding

伊万·哈维尔（Ivan Havel）于1984年提出一项猜想：顶点数为2ⁿ且最大度不超过3的任意树，为n维超立方体（hypercube）的生成树（spanning tree）当且仅当其二分划分类（bipartition classes）的大小相等。四十载光阴已逝，该问题至今仍悬而未决；当n≤4时，该命题已通过计算机辅助验证，而对于更高维度，其正确性仅在少数特殊情形下得到证实。本数据集提供了n=5时哈维尔猜想正确性的机器可验证证明。本次提交的文件包含以下内容：1. computed_solution：存储n=5维度下哈维尔猜想证明的文件；2. program.zip：包含用于计算该证明的程序及其文档的归档文件，其中包含一个可接收以Graphviz格式呈现的、满足该猜想假设的2⁵顶点树，并输出所需嵌入的函数。