Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Van der Waerden's Theorem


view this post on Zulip Email Gateway (Jun 23 2021 at 10:52):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce yet another new entry, Van der Waerden's Theorem, by Katharina Kreuzer and Manuel Eberl:

This article formalises the proof of Van der Waerden's Theorem from Ramsey theory. Van der Waerden's Theorem states that for integers k and l there exists a number N which guarantees that if an integer interval of length at least N is coloured with k colours, there will always be an arithmetic progression of length l of the same colour in said interval. The proof goes along the lines of Swan. The smallest number N[k,l] fulfilling Van der Waerden's Theorem is then called the Van der Waerden Number. Finding the Van der Waerden Number is still an open problem for most values of k and l.

It’s another contribution to our collection of results on Ramsey theory.

And here’s a New Yorker article on Frank Ramsey, who died over 90 years ago at the age of 26: https://www.newyorker.com/magazine/2020/05/04/the-man-who-thought-too-fast

Larry Paulson


Last updated: Jul 15 2022 at 23:21 UTC