Email Gateway (Aug 22 2022 at 20:54): Email Gateway (Aug 22 2022 at 20:54):From: Lawrence Paulson <lp15@cam.ac.uk>
In HOL/Library/Ramsey.thy, we have the 2-colour case of Ramsey’s theorem. However, this isn’t the general finite case. Is anyone aware of a formalisation of the full finite version of the theorem?
Larry
Email Gateway (Aug 22 2022 at 20:54):From: Mario Carneiro <di.gama@gmail.com>
I have a metamath formalization of this theorem, if you care for it:
http://us.metamath.org/mpeuni/ramcl.html
Mario Carneiro
Email Gateway (Aug 22 2022 at 20:54):From: Mario Carneiro <di.gama@gmail.com>
It is also one of the Formalizing 100 Theorems list, and you can find other
formalizations there: http://www.cs.ru.nl/~freek/100/#31
Last updated: Apr 20 2024 at 01:05 UTC