Formal Verification of the Empty Hexagon Number

Stream: general

[Mario Carneiro]

Our joint paper (coauthored with @Bernardo Anibal Subercaseaux Roa , @Wojciech Nawrocki , @James Gallicchio, @Cayden Codel, @Marijn Heule) is now on ArXiv: https://arxiv.org/abs/2403.17370

[Kevin Buzzard]

I know nothing about this problem but just to comment that when trying to figure out what it is from the paper, the phrase "They constructed (and solved) a formula ϕ whose
unsatisfiability implies that every set of 30 points, without three in a common line, must
contain an empty convex hexagon." on p2 confused me for a bit until I realised you must presumably be talking about 30 points in a plane (unless I'm still confused). I suspect that this is obvious to all the authors.

[Mario Carneiro]

Ah. yes

[Mario Carneiro]

The whole problem takes place in $\mathbb{R}^2$

[Mario Carneiro]

The usage of "in general position" in this paper is also not exactly what is meant by the term in other parts of mathematics: it means no three points are on a line

[Michael Stoll]

"In general position" usually means what you need it to mean...

[Kevin Buzzard]

No 5 on a conic was the thing that sprang to mind after Mario's comment, but because he's only doing "linear geometry" not algebraic geometry this is irrelevant

[Mario Carneiro]

The talk at ITP was not recorded (only visible to remote participants), but the slides from it are now available:
EmptyHexagon-slides.pdf