The honeycomb puzzle now has an answer for every size. The author found the proof with the help of AI and it was machine-checked by the proof assistant Lean; an independent review is still pending. Here it is explained without jargon.
A magic hexagon is a number puzzle played on honeycomb cells. The proof that such hexagons exist in every size was found with the help of AI and machine-checked by Lean. The automated proof search took a few hours of computing time. What is meant here is explicitly the mathematical puzzle and not the identically named term from economic policy.
This article first explains what the puzzle demands and traces the path from the first hexagon to the proof. The proof idea then follows in five building blocks, each with a figure. The end deals with the question of why a computer-checked proof can be trusted, what a human still has to check, and which numbers and facts stand behind the result.
Magic hexagon: what the number puzzle demands
The playing field is a honeycomb figure shaped like a regular hexagon. Its size is called order n and states how many cells lie on one side. A hexagon of order n consists of 3n(n−1)+1 cells. For n = 3 that is 19 cells, for n = 10 already 271.
Integers are written into the cells so that every straight row has the same sum. Rows are counted in all three directions of the honeycomb figure. In each direction there are 2n−1 rows. The shortest ones at the edge have n cells, the middle one has 2n−1 cells.
The most famous magic hexagon carries the numbers 1 to 19 and has order 3. Every row sums to 38. It is the classic hexagon, and for the numbers starting at 1 it is the only size in which the puzzle works out. A simple divisibility argument shows that the required row sum is a whole number only for n = 1 and n = 3. For all other orders, the classic variant therefore fails right from the start.
That is why the new work revolves around a related variant. Instead of starting at 1, the integers from −K to K are used, each exactly once. Here K = 3n(n−1)/2. For n = 3 these are the numbers −9 to 9, for n = 10 the numbers −135 to 135. Every row sums to 0, and the 0 sits in the centre.
The puzzle sounds harmless but is hard. The number of possible fillings grows so fast with n that trying them out on a computer does not get far. What was needed was therefore a blueprint that works for every size, and a proof that this blueprint really always works out.
From the puzzle of 1887 to the largest known hexagon: the story
The original problem comes from Ernst von Haselberg and is usually dated to 1887. Some sources give 1888; the primary source was not consulted. Later, by his own account, Adams rediscovered the classic hexagon in 1957 and made it known through Martin Gardner's column. That this solution is the only one up to rotation and reflection was proven by Charles W. Trigg, published in 1964. A collection on this is kept by Bielefeld University, and an overview is offered by Wolfram MathWorld.
The variant with consecutive integers and sum 0 came into view later. Between 2004 and 2006, orders 4 to 8 were found, order 6 in October 2004, orders 7 and 8 in 2006. Until 2006, only order 8 was known as the largest solution. Smaller orders had already been solved by then. An overview with sources is provided by the German Wikipedia, whose dates are partly without citation.
In 2024, Dr. DSGVO, the author of this blog, found a solution of order 9 with AI. At the time, that was the largest known solution.
On 2 August 2026, Konstantin Gukov then published a pattern on his page New magic hexagons. He searched for solutions up to order 21 and recognized that a construction rule for arbitrarily large hexagons can probably be derived from them. Gukov described an algorithm and a proof sketch that was supposed to take effect from order 114 onwards. He points out himself that this sketch is not formalized in Lean and not independently checked. The proof was therefore still missing.
For this gap, a proof for all orders from 3 is now available. It was produced with AI and is documented in a description dated 21 October 2026. It is machine-checked by Lean, an independent review is still pending, and the Lean files are not yet publicly linked. More on that later.
About 140 years lie between the first hexagon and the proof for all sizes.
Magic hexagons for all sizes: what is proven
What is proven: for every order n from 3 there is a magic hexagon with the numbers from −K to K in which every row in all three directions has sum 0. The strengthened version, in which the 0 additionally sits in the centre, is also proven. There is no upper limit. Gukov's sketch only takes effect from order 114; the orders before that remained open without the last building block.
Are there magic hexagons for every size?
Coverage is staggered. Order 2 is impossible because the seven numbers −3 to 3 cannot be distributed suitably. This part is not part of the Lean proof. For orders 3 to 6, finished hexagons exist that Lean re-checked number by number. For orders 7 to 61, a general blueprint applies, complemented by one checked solution of a sub-puzzle each. For orders 62 to 118 the same holds, except that the necessary lists were recomputed and checked. From order 119, a fixed blueprint suffices that is proven in general for every n.
Two main theorems summarize this. The first states that for every n from 3 there is a magic hexagon of order n. The second says the same for the strengthened version with the 0 in the centre. Both theorems have no assumption other than n ≥ 3.
The proof in five building blocks: overview
The proof can be imagined as a ladder. Each building block shrinks the task until only a seating plan on a bench remains. Building blocks 1 to 4 were already available in checked form. New is the fifth building block, the seating plan for every size. It completes the proof.
The following sections go through the building blocks in order. The first three are intuitive, the last two may be a little more technical. All calculations were checked by Lean, so the ideas are enough in the text.
Building block 1: one sixth is enough, because the opposite holds the negative
The whole hexagon does not have to be planned, one sixth is enough. Every cell has an opposite cell that lies mirrored through the centre. If the number a is in one cell, −a goes into the opposite cell. This uses up every number together with its negative, and the 0 is left for the centre.
This has a practical consequence for the rows. The mirrored row has exactly the negative sum. If one row is balanced, so is its mirror image. Rows through the centre are balanced automatically.
The hexagon falls into six equal triangles around the centre. Three of them are opposite-cell triangles: their numbers follow from the mirroring through the centre with reversed sign. Two more are copies of the sixth triangle rotated by 120 degrees and receive closely related numbers. What remains is a single free triangle with T = n(n−1)/2 cells. For n = 10 that is 45 instead of 271 cells.
The condition "every row has sum 0" thereby becomes a condition on this triangle. For each row, a weighted sum of its entries must be zero. This sum is called the balance of the row in what follows.
Building block 2: every number becomes base plus digit
In the second step, every number is split into two parts, a base and a digit. Both parts are balanced separately. Because row sums simply add up when numbers are added, the hexagon is magic as soon as both parts are balanced on their own.
For this, the supply of numbers 1 to 3T is divided into groups of three: k, T+k and 2T+k for k from 1 to T. Each group is the base T+k plus T times a digit, where the digit is −1, 0 or 1. For the hexagon of order 3, T = 3 and the supply runs from 1 to 9. Base 4 yields 1, 4 and 7, base 5 yields 2, 5 and 8, base 6 yields 3, 6 and 9.
The task thus falls apart into two independent puzzles. The first is a digit field of −1, 0 and 1 with balance zero in every row. The second is a base field in which the amounts T+1 to 2T are distributed and given signs so that the balance of every row is zero.
Building block 3: the digit field grows like a ladder
The digit field is completely solved for every order from n = 5, by induction in steps of three. Everyone knows the principle from a ladder: whoever has the first rung and a rule for the step to the next reaches every rung.
First there are finished, balanced digit fields for the radii 4, 5 and 6. The radius is n−1. Then an extension rule applies: a balanced digit field can be extended by three new layers at the edge. The new layers are patterned so that they cancel each other in every row. From 4 this leads to 7, 10, 13 and on, from 5 to 8, 11 and on, from 6 to 9, 12 and on. Every radius from 4 is thereby reached.
This part costs hardly any computing time when checking. It does, however, solve only the first of the two sub-puzzles; the base field remains open.
Building block 4: target distances that balance each other
The base field is not searched for directly. Instead, for each pair of cells it is first fixed by how much its two bases should differ. These target distances are proven in general for all orders from n = 13.
Almost all cells of the triangle form pairs that lie mirrored on its centre axis. One cell of a pair gets a minus, the other a plus. In the balance, only the difference between the two amounts remains; the common part T drops out. So all that matters is the distance between the two ranks. The rank is simply the seat number: the base T+k has rank k.
The target distances arise in several steps. There are associativity circuits: small patterns of four cell pairs with weights +1 and −1 and balance zero in every row. The name comes from the rule of arithmetic that, in sums, the brackets can be moved without changing the result. Every sum of such patterns also has balance zero. From many patterns a master field arises in which no cell pair gets distance 0. A distance of 0 would be unusable, because two cells may never carry the same number.
The cells on the centre axis have no partner. They get the smallest ranks 1, 2, 3 and so on, and the master field balances exactly their contribution. The diagonal cells additionally carry the share T, which does not cancel out. It is balanced by two branching chains of cell pairs, the forests. Their distances are enlarged by about T/2, so by T together.
The result is a complete set of target distances with balance zero in every row, none of them zero. Most distances are small and lie at 12 at most. The cells of the first row have distances up to about 2n, the pairs of the forests distances close to T/2.
Building block 5: the seating plan for every size
Finally, the ranks 1 to T actually have to be distributed so that every cell pair gets exactly its target distance. From n = 119 this is done with a fixed blueprint; below that, with lists found by computer and checked by Lean.
This can be pictured as a seating plan on a long bench with T seats. The diagonal cells sit at fixed places on the first seats 1, 2, 3 and so on. Each cell pair needs two seats at the prescribed distance. No seat may be occupied twice. Exactly n−1 seats stay free. These go to the edge cells without a partner, for which any seat will do.
The decisive trick is blocks. Pairs with the same distance g can be stacked without gaps. For g = 3, the pairs (1, 4), (2, 5) and (3, 6) fill seats 1 to 6 without a gap. In general, g pairs with distance g fill exactly 2g consecutive seats, then the next block follows. This way each distance group wastes at most g−1 seats at the end of its last block. The groups with the distances 1 to 12 together cost at most 0+1+…+11 = 66 seats.
The bench is divided from front to back into five zones. In the first zone sits the diagonal. Next comes the star window, in which a special row of pairs is nested like rainbows and pairs with the distances 6 and 8 fit into the gaps. In the forest window sit pairs with very large distances, whose partners land far back in a reserved area. After that come the residue classes, that is, all remaining pairs with the distances 1 to 12 in blocks. Finally the n−1 edge cells take the seats that are left.
Why does the blueprint only work from n = 119? The bench is almost exactly full. Only as many seats may stay free as there are edge cells without a partner, namely n−1. The blueprint loses at most 117 seats: 18 in the star window, 66 in the blocks, 21 in the forest window and 12 when skipping. So it works out as soon as n−1 is at least 118. At n = 119, 118 seats are free and at most 117 are lost, so one seat of reserve remains.
For the smaller sizes, a computer program searched for suitable seating plans and saved them as lists of numbers. These lists are called certificates. Lean re-checks each certificate itself instead of trusting the search program.
Why the proof can be trusted: Lean checks every step
The proof is not only written down but checked line by line by a proof checker. Lean is a programming language for mathematical proofs. Every inference is written down so precisely that the computer can recompute it. There are no gaps or an "obviously" there. An error would make the translation abort.
It uses Mathlib, the large shared library of already checked mathematics for Lean, for example for rules of arithmetic with finite sets and sums. Not a single "sorry" occurs in the finished proof. That is the name of the placeholder in Lean with which a step can be skipped for the time being. There is also no custom axiom (an unproven basic assumption) and no trust in translated program code. At the end Lean can list which basic assumptions a theorem rests on. Here there are only the three usual ones on which practically all of Mathlib is built: propext, Classical.choice and Quot.sound.
The Python programs that found the certificates and the blueprint do not have to be free of errors. A wrong certificate or a wrong blueprint would be rejected by Lean. That is the real gain in using AI and search programs: the tools may guess, the check is still strict.
The computer guarantees that the theorem follows from its definitions. Whether the definition means what is understood by a magic hexagon must be checked by a human.
What a human has to check: the definition in five lines
One limit applies to every computer-checked proof: the definition at the start is not checked but assumed. In the present case the definition is only five lines long, and in everyday language it says this: there is a filling of the cells with integers. No two cells carry the same value. The values used are exactly the numbers from −K to K. Every row in each of the three directions has sum 0. In the strengthened version the 0 additionally sits in the centre.
Three possible loopholes are ruled out. First, cells and numbers match: the hexagon has 3n(n−1)+1 cells, and from −K to K there are exactly as many numbers, so "each number exactly once" is enforced. Second, values outside the hexagon do not count; all conditions refer only to cells inside the hexagon. Third, rows outside the hexagon are empty, their sum is automatically 0, which is harmless. The formula for K uses integer division, which is unproblematic because n(n−1) is always even.
The check also revealed a gap that has since been closed. The original definition did not explicitly require the 0 in the centre. The construction always delivers it, because mirrored cells carry opposite values. Even so, there is now the strengthened definition with the additional condition that the centre is 0, and the second main theorem proves it for all n from 3.
Some residual trust remains, as with any formal proof. It concerns the small kernel of Lean and the basic definitions of Mathlib, for example for sums and intervals. A pre-release version of Lean 4 was used. In addition, the check has so far run in a single environment. It becomes safer when someone independently compiles the files on their own machine. Optionally, a separate checking program such as lean4checker can verify the finished proof files once more. For small sizes, a concrete hexagon can also be output and re-calculated by hand. That proves nothing additional, but shows vividly that the definition captures what is meant.
Numbers and facts about the proof
On the statement: a magic hexagon with sum zero is proven for every order n from 3, also with the 0 in the centre. Finished hexagons exist for n = 3 to 6. For n = 7 to 118, certificates deliver the solution of the base puzzle, of which 57 are new, namely those for n = 62 to 118. The general blueprint applies from n = 119, which corresponds to radius 118. It loses at most 117 seats and leaves at least one seat of reserve at n = 119. The largest certificate order is n = 118, which corresponds to 6,903 cells in the triangle.
On size: building blocks 1 to 4 and the certificates up to n = 61 are combined in one file that has 2,713 lines. Building block 5 consists of 40 files with around 7,000 lines. The largest memory requirement is 5.9 gigabytes, for a file on the first row of the blueprint. Lean 4 in the pre-release version v4.35.0-rc4 and Mathlib were used. Only propext, Classical.choice and Quot.sound appear as axioms, and there are no open gaps.
On computing time: rebuilding building block 5 takes about 38 minutes, and the certificates need about 23 minutes in parallel. Individual files take considerably longer. The file with building blocks 1 to 4 needs 460 seconds, the auxiliary file with the formulas of the target distances 897 seconds, the certificates for n = 62 to 89 another 437 seconds and those for n = 90 to 117 another 927 seconds. The files on the first row take about 18 minutes together. These times describe the rebuild of the finished check. The entire automated proof effort, with search and development, took a few hours.
On the preliminary tests: before the Lean proof, the blueprint was tested numerically as an exact replica of the definitions for the radii 118 to 450. The auxiliary statements were checked up to radius 20,000. These tests were only a preliminary check; the proof itself is the Lean text.
What comes next: open questions and context
Gukov's work and the Lean proof complement each other. Gukov supplied the pattern, the construction and a sketch with the limit 114. The sketch did not recompute the gaps of the first row and of the forests. Set naively, about 2n to 3n seats would have been missing there together, more than the permitted n−1. The Lean proof starts at exactly this point. It delivers formulas for the target distances, a packing plan with at most 117 lost seats instead of 2n to 3n, and new certificates for orders 62 to 118. With that, all orders from 3 are covered.
What remains open for now is the independent check: a rebuild on a foreign machine (already provided by the author), ideally with lean4checker, and a review by experts. The Lean files are not yet publicly linked in this description. In addition, Gukov poses a question on his page that the proof does not answer: why do the cell values look random while the associated potential fields look smooth? Further variants of the puzzle are conceivable, but nothing is promised.
A puzzle that began with a honeycomb figure of 19 cells is solved for every size. It took first a human's idea, then AI as searcher and proof assistant, and finally a checker that believes none of the parties involved but recomputes every step.
My name is Klaus Meffert. I have a doctorate in computer science and have been working professionally and practically with information technology for over 30 years. I also work as an expert in IT & data protection. I achieve my results by looking at technology and law. This seems absolutely essential to me when it comes to digital data protection. My company, IT Logic GmbH, also offers consulting and development of optimized and secure AI solutions.
