A Formal Proof of R(4,5)=25

Thibault Gauthier, Chad E. Brown

In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The author…