A simple unit-distance embedding of the Heawood graph

Stream: mathlib4

[Jeremy Tan]

In 1972 Chvátal voiced a suspicion that the Heawood graph was not a unit-distance graph – a graph embeddable in the Euclidean plane such that all adjacent vertex pairs are distance 1 apart.

This suspicion was disproved in 2009 by Eberhard Gerbracht (see paper), but his 11 embeddings, and all those published by later authors, only exist in numerical form or have very high degree minimal polynomials for their coordinates.

In August 2025 I found, using my Shibuya utility and some hand work, the following much simpler embedding:
heawood-ud.png
The minimal polynomials of its coordinates are at most cubic.

Now I have found time to formalise this embedding, and the result is at #32684. That PR obviously isn't intended to be merge-ready, but I'd like to hear your thoughts on my code, written with no AI help whatsoever.

[Kevin Buzzard]

Nice work! Why not put Heawood.lean in Mathlib's Counterexamples directory and link to the relevant papers in the module docstring? Then I could see it ultimately making it into mathlib proper. A not-merge-ready PR will just rot.

[Jeremy Tan]

Kevin Buzzard said:

Why not put Heawood.lean in Mathlib's Counterexamples directory and link to the relevant papers in the module docstring?

OK, I've done that

[Jeremy Tan]

Another reference added, and the module docstring for the Basic.lean file has been fleshed out

[Bhavik Mehta]

This is a nice result!

[Junyan Xu]

I just found that @Moritz Firsching asked this MO question 9+ years ago, and this embedding partially answers his question (it's symmetric but not faithful, by inspection non-edges 1-5, 8-12, 2-11 are also distance 1).

[Junyan Xu]

I can't figure out what the last sentence of Gerbracht's paper mean; is his "regular" embedding same as "faithful"? Wikipedia's definition of unit-distance graphs includes the faithfulness condition, but it also states the notion is often prefixed with "strict" or "faithful" in the literature.
image.png

[Moritz Firsching]

Jeremy Tan said:

...and all those published by later authors, only exist in numerical form or have very high degree minimal polynomials for their coordinates.

What is the distance of vertices 2 and 11 in your graph? If it is $1$, it might be the essentially the same embedding you found compared to this one:
sum3_5zero.svg
from the mentioned mathoverflow question?
I didn't check in detail, but the drawings look similar, and both have minimal polynomials of degree $\le 3$
I provided exact coordinates at the time: https://firsching.ch/mo/heawood/sum3_5zero.txt

[Junyan Xu]

Oh yeah, they do look the same. I only skimmed through the MO post and missed that your first example has max degree 3.

[Jeremy Tan]

Junyan Xu said:

I can't figure out what the last sentence of Gerbracht's paper mean; is his "regular" embedding same as "faithful"? Wikipedia's definition of unit-distance graphs includes the faithfulness condition, but it also states the notion is often prefixed with "strict" or "faithful" in the literature.
image.png

By regular Gerbracht means "there is no vertex lying in the strict interior of an edge"

[Jeremy Tan]

Moritz Firsching said:

Jeremy Tan said:

...and all those published by later authors, only exist in numerical form or have very high degree minimal polynomials for their coordinates.

What is the distance of vertices 2 and 11 in your graph? If it is $1$, it might be the essentially the same embedding you found compared to this one:
sum3_5zero.svg
from the mentioned mathoverflow question?
I didn't check in detail, but the drawings look similar, and both have minimal polynomials of degree $\le 3$
I provided exact coordinates at the time: https://firsching.ch/mo/heawood/sum3_5zero.txt

OK, what do I do now? The MO post has never been mentioned elsewhere. This is very deflating for me

[Jeremy Tan]

I spent quite a lot of effort to find the embedding only to see that someone else came up with it years ago

[Patrick Massot]

This happens in research from time to time. It is no fun at all but it’s still part of the game.

[Moritz Firsching]

Sorry, I didn't mean to cause trouble with this. I didn't realize that anybody would be interested in these kind of embeddings (and the mathoverflow post didn't receive much attention). It is not entirely true that is has "never been mentioned elsewhere": https://dustingmixon.wordpress.com/2018/04/14/polymath16-first-thread-simplifying-de-greys-graph/
https://dustingmixon.wordpress.com/2018/04/14/polymath16-first-thread-simplifying-de-greys-graph/#comment-4269

I'm happy to explain how I came up with these embeddings. From your commit that is linked in the pr description it is not quite clear to me if you used the same or a similar method or not.
The system it underdetermined, therefore I added the symmetry constraint and one additional constraint (x[3] + x[5]). Then I used mpmath's findroot to get many digits of a numerical solution (where in this case probably 37 decimal digits suffice). Next I used pslq (algdep) to get the minimal polynomials and then checked with exact arithmetic in the field of of algebraic real numbers (AA). I'd gladly re-write the code for this in a somewhat clean way if anybody is interested.

In any case, I do suspect that there might be faithful embedding of degree lower than 21, and it would be nice to see it, hence the mathoverflow question.

[Jeremy Tan]

Moritz Firsching said:

From your commit that is linked in the pr description it is not quite clear to me if you used the same or a similar method or not.

There is a script in my Shibuya repository which I used to find nearly all the unit-distance embeddings there. It looks for subgroups of C_n and D_n in the input graph's automorphism group, then maps said subgroup to a representation in the Euclidean plane, then randomly drops points and optimises the resulting equations until they are all satisfied

[Jeremy Tan]

https://github.com/Parcly-Taxel/Shibuya/blob/main/shibuya/graphs/embeddingsearch.py

[Jeremy Tan]

The subgroup is also an input to the program, by the way

[Jeremy Tan]

I found planar unit-distance embeddings not just for the Heawood graph, but all cubic symmetric graphs to 120 vertices, as well as the Gray graph, Holt graph, snarks and more

[Jeremy Tan]

I used to have your degree-21 embedding in Shibuya (extracted from Mathematica GraphData) until I found the cubic one

[Moritz Firsching]

Very nice! This seems like a more disciplined approach. Here's a quickly drafted sagemath jupyter notebook as a proof of concept, that does the calculation for one specific symmetry of the Heawood graph as described above: https://github.com/mo271/mo271.github.io/blob/main/mo/heawood/Heawood_embedding.ipynb