Finite projective planes of order 10

Stream: maths

[Judith Ludwig]

Hi everyone. I'm talking to high school students next week about the maths behind the card game dobble (spot it!), i.e. finite projective planes. I want to mention the result of Lam, Thiel and Swiercz (https://www.cambridge.org/core/journals/canadian-journal-of-mathematics/article/nonexistence-of-finite-projective-planes-of-order-10/EBD5E851090B1983978BBC6FE18D2A3F) that no finite projective planes of order 10 exist. They show this via a computer search. They also talk about the possibilty of software-errors asking at the end of the paper that they "hope that someone else will do an independent verification of the results". Searching for this I found https://arxiv.org/abs/2012.04715 which "certifies" the earlier work (I don't understand what this means), but they write: Our work does not provide a completely formal proof of the nonexistence of a projective plane of order ten because we rely on results that currently have no formal computerverifiable proofs. I was wondering whether this is the state of the art, or whether there have been developments in some of the proof-assistants towards (the possibilty of) a formal verification? Does anyone know? (I hope this is not off topic, if there is a better stream for this question please let me know).

[Riccardo Brasca]

Hi Judith! This stream is perfectly fine for your question.

We have this file about projective planes, so there is something in Mathlib. Let me tag the author of the file @Thomas Browning

[Riccardo Brasca]

Concerning the paper, I think they certify in the sense they give something a software (like maple or whatever) can verify, not a proof in a proof assistant. But I can be very wrong.

[Patrick Massot]

We can try to ping @Marijn Heule to comment on this, but he isn't very often here. It is more likely than someone else from CMU can help.

[Thomas Browning]

I don't know if any further work in Lean beyond the file I wrote (we don't even have examples of finite projective planes yet)

[Patrick Massot]

In any case, anything that requires a SAT solver is currently beyond the reach of Lean. But there are people working to bridge the gap. This also applies to other interactive theorem provers.

[Patrick Massot]

See for instance the work of Chantal Keller, in particular https://smtcoq.github.io/.

[Kevin Buzzard]

I'm quite surprised that the computer scientists' eyes didn't light up at that proof back in the 90s.

[Alex Kontorovich]

And by the way, we still (30 years, and a lot of computational power later) don't know about projective planes of order 12, right?

[Judith Ludwig]

thanks for all the replies!
Yes, my understanding is that order 12 ist still open.