Unverified bounds

These are the best bounds from the literature that no certificate matches yet, for the families of constants that accept certificates. Each one is a chance to turn a published bound into a verified one.

A Witness bound can be certified by giving the construction itself, which is often in the cited source or its ancillary files. A Lean proof bound needs a formal proof that no better construction exists, which is usually much harder.

This list is also available as YAML, JSON, CSV or TSV.

Group	Witness	Lean proof
Minimal superpermutation problem	4	9
Optimal Golomb rulers	0	28
Cages	69	27
Coil-in-the-box	0	7
Degree-diameter problem	143	7
Snake-in-the-box	0	8
Ramsey numbers	50	70
Schur numbers	1	5
Van der Waerden numbers	28	7
Weak Schur numbers	3	4
Arrangements of lines in the affine plane	1	8
Arrangements of lines in general position	2	9
Circle packing in an equilateral triangle	0	7
Kissing numbers	12	24
Packing unit squares in a square	0	91

Minimal superpermutation problem

Constant	Literature	Verified	Evidence	Source
Minimal superpermutation length $L(6)$	$\le 872$	$\le 873$	Witness	Houston, R. (2014). Tackling the minimal superpermutation problem. arXiv preprint arXiv:1408.5108.
Minimal superpermutation length $L(7)$	$\le 5905$	$\le 5913$	Witness	Andrei Teodorescu, n=7 superpermutation of length 5905, Superpermutators Google Group, 2026-08-17
Minimal superpermutation length $L(8)$	$\le 46205$	none	Witness	Superpermutations - Greg Egan
Minimal superpermutation length $L(9)$	$\le 408966$	none	Witness	Superpermutations - Greg Egan
Minimal superpermutation length $L(1)$	$\ge 1$	none	Lean proof	Trivial or easy according to the secondary source.
Minimal superpermutation length $L(2)$	$\ge 3$	none	Lean proof	Trivial or easy according to the secondary source.
Minimal superpermutation length $L(3)$	$\ge 9$	none	Lean proof	Superpermutations - Greg Egan
Minimal superpermutation length $L(4)$	$\ge 33$	none	Lean proof	Superpermutations - Greg Egan
Minimal superpermutation length $L(5)$	$\ge 153$	none	Lean proof	Ben Chaffin in 2014
Minimal superpermutation length $L(6)$	$\ge 867$	none	Lean proof	Anonymous 4chan poster, R. Houston, J. Pantone and V. Vatter. A lower bound on the length of the shortest superpattern (2018).
Minimal superpermutation length $L(7)$	$\ge 5884$	none	Lean proof	Anonymous 4chan poster, R. Houston, J. Pantone and V. Vatter. A lower bound on the length of the shortest superpattern (2018).
Minimal superpermutation length $L(8)$	$\ge 46085$	none	Lean proof	Anonymous 4chan poster, R. Houston, J. Pantone and V. Vatter. A lower bound on the length of the shortest superpattern (2018).
Minimal superpermutation length $L(9)$	$\ge 408246$	none	Lean proof	Anonymous 4chan poster, R. Houston, J. Pantone and V. Vatter. A lower bound on the length of the shortest superpattern (2018).

Optimal Golomb rulers

Constant	Literature	Verified	Evidence	Source
Optimal Golomb ruler $G(1)$	$\ge 0$	none	Lean proof	Trivial or easy according to the secondary source.
Optimal Golomb ruler $G(2)$	$\ge 1$	none	Lean proof	Trivial or easy according to the secondary source.
Optimal Golomb ruler $G(3)$	$\ge 3$	none	Lean proof	Trivial or easy according to the secondary source.
Optimal Golomb ruler $G(4)$	$\ge 6$	none	Lean proof	Trivial or easy according to the secondary source.
Optimal Golomb ruler $G(5)$	$\ge 11$	none	Lean proof	J.P. Robinson and A.J. Bernstein, A class of binary recurrent codes with limited error propagation, IEEE Transactions on Information Theory 13 (1967) 106-113.
Optimal Golomb ruler $G(6)$	$\ge 17$	none	Lean proof	J.P. Robinson and A.J. Bernstein, A class of binary recurrent codes with limited error propagation, IEEE Transactions on Information Theory 13 (1967) 106-113.
Optimal Golomb ruler $G(7)$	$\ge 25$	none	Lean proof	J.P. Robinson and A.J. Bernstein, A class of binary recurrent codes with limited error propagation, IEEE Transactions on Information Theory 13 (1967) 106-113.
Optimal Golomb ruler $G(8)$	$\ge 34$	none	Lean proof	William Mixon, unpublished, reported in M. Gardner, Mathematical Games, Scientific American 226(3) (1972) 108-112.
Optimal Golomb ruler $G(9)$	$\ge 44$	none	Lean proof	William Mixon, unpublished, reported in M. Gardner, Mathematical Games, Scientific American 226(3) (1972) 108-112.
Optimal Golomb ruler $G(10)$	$\ge 55$	none	Lean proof	William Mixon, unpublished, reported in M. Gardner, Mathematical Games, Scientific American 226(3) (1972) 108-112.
Optimal Golomb ruler $G(11)$	$\ge 72$	none	Lean proof	William Mixon, unpublished, reported in M. Gardner, Mathematical Games, Scientific American 226(3) (1972) 108-112.
Optimal Golomb ruler $G(12)$	$\ge 85$	none	Lean proof	J.P. Robinson, Optimum Golomb rulers, IEEE Transactions on Computers C-28 (1979) 943-944.
Optimal Golomb ruler $G(13)$	$\ge 106$	none	Lean proof	J.P. Robinson, Addendum to 'Optimum Golomb rulers', IEEE Transactions on Computers C-32 (1983) 201.
Optimal Golomb ruler $G(14)$	$\ge 127$	none	Lean proof	J.B. Shearer, Some new optimum Golomb rulers, IEEE Transactions on Information Theory 36 (1990) 183-184.
Optimal Golomb ruler $G(15)$	$\ge 151$	none	Lean proof	J.B. Shearer, Some new optimum Golomb rulers, IEEE Transactions on Information Theory 36 (1990) 183-184.
Optimal Golomb ruler $G(16)$	$\ge 177$	none	Lean proof	J.B. Shearer, Some new optimum Golomb rulers, IEEE Transactions on Information Theory 36 (1990) 183-184.
Optimal Golomb ruler $G(17)$	$\ge 199$	none	Lean proof	W. Olin Sibert in 1993, unpublished.
Optimal Golomb ruler $G(18)$	$\ge 216$	none	Lean proof	W. Olin Sibert in 1993, unpublished.
Optimal Golomb ruler $G(19)$	$\ge 246$	none	Lean proof	A. Dollas, W.T. Rankin and D. McCracken, A new algorithm for Golomb ruler derivation and proof of the 19 mark ruler, IEEE Transactions on Information Theory 44 (1998) 379-382.
Optimal Golomb ruler $G(20)$	$\ge 283$	none	Lean proof	M. Garry, D. Vanderschel et al., In Search Of The Optimal 20, 21 & 22 Mark Golomb Rulers (distributed search), 20 marks.
Optimal Golomb ruler $G(21)$	$\ge 333$	none	Lean proof	M. Garry, D. Vanderschel et al., In Search Of The Optimal 20, 21 & 22 Mark Golomb Rulers (distributed search), 21 marks.
Optimal Golomb ruler $G(22)$	$\ge 356$	none	Lean proof	M. Garry, D. Vanderschel et al., In Search Of The Optimal 20, 21 & 22 Mark Golomb Rulers (distributed search), 22 marks.
Optimal Golomb ruler $G(23)$	$\ge 372$	none	Lean proof	M. Garry, D. Vanderschel et al., distributed search for the optimal 23 mark Golomb ruler.
Optimal Golomb ruler $G(24)$	$\ge 425$	none	Lean proof	distributed.net, OGR-24 completed (project started February 2000; final stub verified 2004-10-13), announced 2004-11-01.
Optimal Golomb ruler $G(25)$	$\ge 480$	none	Lean proof	distributed.net, OGR-25 completed, announced 2008-10-25.
Optimal Golomb ruler $G(26)$	$\ge 492$	none	Lean proof	distributed.net, OGR-26 completed, announced 2009-02-24.
Optimal Golomb ruler $G(27)$	$\ge 553$	none	Lean proof	distributed.net, OGR-27 completed, announced 2014-02-25.
Optimal Golomb ruler $G(28)$	$\ge 585$	none	Lean proof	distributed.net, OGR-28 completed, announced 2022-11-23.

Cages

Constant	Literature	Verified	Evidence	Source
Cage order $n(3,9)$	$\le 58$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,10)$	$\le 70$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,11)$	$\le 112$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,12)$	$\le 126$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,13)$	$\le 272$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,14)$	$\le 384$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,15)$	$\le 620$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,16)$	$\le 936$	none	Witness	Exoo, G., Goedgebeur, J., Jooken, J., Stubbe, T., & Van den Eede, G. (2026). New Small Regular Graphs of Given Girth: the Cage Problem and Beyond. The Electronic Journal of Combinatorics, 33(3), P3.48.
Cage order $n(4,5)$	$\le 19$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(4,7)$	$\le 67$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(4,9)$	$\le 270$	none	Witness	Exoo, G., Goedgebeur, J., Jooken, J., Stubbe, T., & Van den Eede, G. (2026). New Small Regular Graphs of Given Girth: the Cage Problem and Beyond. The Electronic Journal of Combinatorics, 33(3), P3.48.
Cage order $n(4,10)$	$\le 320$	none	Witness	Exoo, G., Goedgebeur, J., Jooken, J., Stubbe, T., & Van den Eede, G. (2026). New Small Regular Graphs of Given Girth: the Cage Problem and Beyond. The Electronic Journal of Combinatorics, 33(3), P3.48.
Cage order $n(4,12)$	$\le 728$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(5,5)$	$\le 30$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(5,7)$	$\le 152$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(5,10)$	$\le 1296$	none	Witness	G. Exoo, Regular graphs of given degree and girth.
Cage order $n(5,11)$	$\le 2688$	none	Witness	G. Araujo-Pardo, On upper bounds of odd girth cages, Discrete Math. 310 (2010) 1622-1626.
Cage order $n(5,12)$	$\le 2730$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(6,5)$	$\le 40$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(6,7)$	$\le 294$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(6,12)$	$\le 7812$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(7,6)$	$\le 90$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(7,8)$	$\le 672$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(7,12)$	$\le 32928$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(8,5)$	$\le 80$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(8,12)$	$\le 39216$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(9,5)$	$\le 96$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(9,7)$	$\le 1152$	none	Witness	G. Araujo-Pardo, On upper bounds of odd girth cages, Discrete Math. 310 (2010) 1622-1626.
Cage order $n(9,8)$	$\le 1170$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(9,11)$	$\le 74752$	none	Witness	G. Araujo-Pardo, On upper bounds of odd girth cages, Discrete Math. 310 (2010) 1622-1626.
Cage order $n(9,12)$	$\le 74898$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(10,5)$	$\le 124$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(10,8)$	$\le 1640$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(10,12)$	$\le 132860$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(11,5)$	$\le 154$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(11,6)$	$\le 240$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(11,8)$	$\le 2618$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(11,12)$	$\le 319440$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(12,5)$	$\le 203$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(12,8)$	$\le 2928$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(12,12)$	$\le 354312$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(13,5)$	$\le 230$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(13,6)$	$\le 336$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(13,8)$	$\le 4342$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(13,12)$	$\le 738192$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(14,5)$	$\le 288$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(14,8)$	$\le 4760$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(14,12)$	$\le 804468$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(15,5)$	$\le 312$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(15,6)$	$\le 462$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(15,8)$	$\le 7648$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(15,12)$	$\le 1957376$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(16,5)$	$\le 336$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(16,6)$	$\le 504$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(16,8)$	$\le 8092$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(16,12)$	$\le 2088960$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(17,5)$	$\le 448$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(17,8)$	$\le 8738$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(17,12)$	$\le 2236962$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(18,5)$	$\le 480$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(18,8)$	$\le 10440$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(18,12)$	$\le 3017196$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(19,5)$	$\le 512$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(19,6)$	$\le 720$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(19,8)$	$\le 13642$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(19,12)$	$\le 4938480$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(20,5)$	$\le 576$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(20,8)$	$\le 14480$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(20,12)$	$\le 5227320$	none	Witness	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,7)$	$\ge 24$	$\ge 22$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,9)$	$\ge 58$	$\ge 46$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,10)$	$\ge 70$	$\ge 62$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,11)$	$\ge 112$	$\ge 94$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,13)$	$\ge 202$	$\ge 190$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,14)$	$\ge 258$	$\ge 254$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,15)$	$\ge 384$	$\ge 382$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(3,16)$	$\ge 512$	$\ge 510$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(4,5)$	$\ge 19$	$\ge 17$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(4,7)$	$\ge 67$	$\ge 53$	Lean proof	Cage (graph theory) - Wikipedia
Cage order $n(5,5)$	$\ge 30$	$\ge 26$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(6,5)$	$\ge 40$	$\ge 37$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(7,6)$	$\ge 90$	$\ge 86$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(8,5)$	$\ge 67$	$\ge 65$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(9,5)$	$\ge 86$	$\ge 82$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(10,5)$	$\ge 103$	$\ge 101$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(11,5)$	$\ge 124$	$\ge 122$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(11,6)$	$\ge 224$	$\ge 222$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(12,5)$	$\ge 147$	$\ge 145$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(13,5)$	$\ge 174$	$\ge 170$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(14,5)$	$\ge 199$	$\ge 197$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(15,5)$	$\ge 230$	$\ge 226$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(16,5)$	$\ge 259$	$\ge 257$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(17,5)$	$\ge 294$	$\ge 290$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(18,5)$	$\ge 327$	$\ge 325$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(19,5)$	$\ge 364$	$\ge 362$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26
Cage order $n(20,5)$	$\ge 403$	$\ge 401$	Lean proof	Dynamic Cage Survey, Geoffrey Exoo and Robert Jajcay, 2013-07-26

Coil-in-the-box

Constant	Literature	Verified	Evidence	Source
Coil-in-the-box $c(2)$	$\le 4$	none	Lean proof	W.H. Kautz, Unit-distance error-checking codes, IRE Transactions on Electronic Computers EC-7 (1958) 179-180.
Coil-in-the-box $c(3)$	$\le 6$	none	Lean proof	W.H. Kautz, Unit-distance error-checking codes, IRE Transactions on Electronic Computers EC-7 (1958) 179-180.
Coil-in-the-box $c(4)$	$\le 8$	none	Lean proof	W.H. Kautz, Unit-distance error-checking codes, IRE Transactions on Electronic Computers EC-7 (1958) 179-180.
Coil-in-the-box $c(5)$	$\le 14$	none	Lean proof	W.H. Kautz, Unit-distance error-checking codes, IRE Transactions on Electronic Computers EC-7 (1958) 179-180.
Coil-in-the-box $c(6)$	$\le 26$	none	Lean proof	D.W. Davies, Longest "separated" paths and loops in an N cube, IEEE Transactions on Electronic Computers EC-14 (1965) 261.
Coil-in-the-box $c(7)$	$\le 48$	none	Lean proof	K.J. Kochut, Snake-in-the-box codes for dimension 7, Journal of Combinatorial Mathematics and Combinatorial Computing 20 (1996) 175-185.
Coil-in-the-box $c(8)$	$\le 96$	none	Lean proof	P.R.J. Östergård and V.H. Pettersson, On the maximum length of coil-in-the-box codes in dimension 8, Discrete Applied Mathematics 179 (2014) 193-200.

Degree-diameter problem

Constant	Literature	Verified	Evidence	Source
Degree-diameter problem $N(3,5)$	$\ge 70$	$\ge 64$	Witness	Alegre, I., Fiol, M. A., & Yebra, J. L. A. (1986). Some large graphs with given degree and diameter. Journal of graph theory, 10(2), 219-224.
Degree-diameter problem $N(3,6)$	$\ge 132$	$\ge 64$	Witness	Geoffrey Exoo, communicated to F. Comellas on May 22, 1998. Construction in G. Exoo, A family of graphs and the degree/diameter problem, J. Graph Theory 37 (2001), 118-124.
Degree-diameter problem $N(3,7)$	$\ge 200$	$\ge 162$	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(3,8)$	$\ge 360$	$\ge 272$	Witness	Jianxiang Chen, 2018
Degree-diameter problem $N(3,9)$	$\ge 600$	$\ge 506$	Witness	Geoffrey Exoo, communicated to F. Comellas on January 28, 2008
Degree-diameter problem $N(3,10)$	$\ge 1250$	$\ge 820$	Witness	Conder, M. (2006). Trivalent (cubic) symmetric graphs on up to 2048 vertices.
Degree-diameter problem $N(4,4)$	$\ge 104$	$\ge 84$	Witness	Nishant Bhakar in August 2026
Degree-diameter problem $N(4,5)$	$\ge 364$	$\ge 205$	Witness	Delorme, C. (1985). Grands graphes de degré et diametre donnés. European Journal of Combinatorics, 6(4), 291-302.
Degree-diameter problem $N(4,6)$	$\ge 760$	$\ge 513$	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(4,7)$	$\ge 1344$	$\ge 1155$	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(4,8)$	$\ge 3243$	none	Witness	Loz, E., & Sirán, J. (2008). New record graphs in the degree-diameter problem. Australasian Journal of Combinatorics, 41, 63.
Degree-diameter problem $N(4,9)$	$\ge 7884$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(4,10)$	$\ge 19306$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(5,3)$	$\ge 72$	$\ge 54$	Witness	Exoo, G. (2001). A family of graphs and the degree/diameter problem. Journal of Graph Theory, 37(2), 118-124.
Degree-diameter problem $N(5,4)$	$\ge 252$	$\ge 210$	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs, orbit graphs and lifts. Zenodo.
Degree-diameter problem $N(5,5)$	$\ge 650$	$\ge 506$	Witness	Rithwik Gupta in September 2026
Degree-diameter problem $N(5,6)$	$\ge 2836$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(5,7)$	$\ge 6000$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(5,8)$	$\ge 18810$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(5,9)$	$\ge 60686$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(5,10)$	$\ge 202550$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(6,3)$	$\ge 120$	$\ge 90$	Witness	Michel de Messieres in October 2026
Degree-diameter problem $N(6,4)$	$\ge 441$	$\ge 355$	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs, orbit graphs and lifts. Zenodo.
Degree-diameter problem $N(6,5)$	$\ge 1518$	$\ge 1395$	Witness	Rajiv, R. (2026). Improved lower bounds for the degree-diameter problem from metacyclic groups, coset graphs and affine lifts. Zenodo.
Degree-diameter problem $N(6,6)$	$\ge 8802$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(6,7)$	$\ge 20400$	none	Witness	Rithwik Gupta in September 2026
Degree-diameter problem $N(6,8)$	$\ge 80050$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(6,9)$	$\ge 331387$	none	Witness	Canale, E., & Rodríguez, A. (2012). On the application of voltage graphs to the degree/diameter problem.
Degree-diameter problem $N(6,10)$	$\ge 1394189$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(7,3)$	$\ge 170$	$\ge 140$	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, orbit graphs and clique substitution. Zenodo.
Degree-diameter problem $N(7,4)$	$\ge 684$	$\ge 602$	Witness	Michel de Messieres in October 2026
Degree-diameter problem $N(7,5)$	$\ge 2810$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(7,6)$	$\ge 12654$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(7,7)$	$\ge 56952$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs, orbit graphs and lifts. Zenodo.
Degree-diameter problem $N(7,8)$	$\ge 264440$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(7,9)$	$\ge 1332774$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(7,10)$	$\ge 6645690$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(8,4)$	$\ge 1100$	$\ge 1029$	Witness	Loz, E., & Sirán, J. (2008). New record graphs in the degree-diameter problem. Australasian Journal of Combinatorics, 41, 63.
Degree-diameter problem $N(8,5)$	$\ge 5334$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs, orbit graphs and lifts. Zenodo.
Degree-diameter problem $N(8,6)$	$\ge 40560$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(8,7)$	$\ge 139679$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(8,8)$	$\ge 802890$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(8,9)$	$\ge 4601361$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(8,10)$	$\ge 26988069$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(9,3)$	$\ge 585$	$\ge 256$	Witness	Delorme, C. (1985). Grands graphes de degré et diametre donnés. European Journal of Combinatorics, 6(4), 291-302.
Degree-diameter problem $N(9,4)$	$\ge 1768$	$\ge 1254$	Witness	Francesc Comellas in October 2026
Degree-diameter problem $N(9,5)$	$\ge 9020$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(9,6)$	$\ge 77418$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(9,7)$	$\ge 309510$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(9,8)$	$\ge 1961496$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(9,9)$	$\ge 13219318$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(9,10)$	$\ge 89658816$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(10,3)$	$\ge 650$	$\ge 366$	Witness	Delorme, C. (1985). Grands graphes de degré et diametre donnés. European Journal of Combinatorics, 6(4), 291-302.
Degree-diameter problem $N(10,4)$	$\ge 2556$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(10,5)$	$\ge 33397$	none	Witness	Rajiv, R. (2026). Large graphs of diameter five from a duality of order four of the split Cayley hexagon H(9). Zenodo.
Degree-diameter problem $N(10,6)$	$\ge 137180$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(10,7)$	$\ge 624690$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(10,8)$	$\ge 4524979$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(10,9)$	$\ge 34913494$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(10,10)$	$\ge 265782337$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(11,2)$	$\ge 106$	$\ge 98$	Witness	Dharunish Yugeswardeenoo in September 2026
Degree-diameter problem $N(11,3)$	$\ge 715$	$\ge 420$	Witness	Delorme, C. (1985). Grands graphes de degré et diametre donnés. European Journal of Combinatorics, 6(4), 291-302.
Degree-diameter problem $N(11,4)$	$\ge 3645$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(11,5)$	$\ge 37628$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(11,6)$	$\ge 186033$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(11,7)$	$\ge 1197748$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(11,8)$	$\ge 9739368$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(11,9)$	$\ge 81961120$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(11,10)$	$\ge 697429356$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(12,3)$	$\ge 810$	$\ge 558$	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(12,4)$	$\ge 6156$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(12,5)$	$\ge 42342$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(12,6)$	$\ge 364032$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(12,7)$	$\ge 2115075$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(12,8)$	$\ge 19218539$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(12,9)$	$\ge 179227730$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(12,10)$	$\ge 1693183778$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(13,3)$	$\ge 972$	$\ge 630$	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(13,4)$	$\ge 6804$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(13,5)$	$\ge 51417$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(13,6)$	$\ge 538740$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(13,7)$	$\ge 3691038$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(13,8)$	$\ge 36275160$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(13,9)$	$\ge 362847996$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(13,10)$	$\ge 3789512750$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(14,3)$	$\ge 1201$	$\ge 791$	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(14,4)$	$\ge 9720$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(14,5)$	$\ge 94186$	none	Witness	Sami Hani Badaoui and Sarah Ellen Mary Vaughan in October 2026
Degree-diameter problem $N(14,6)$	$\ge 824124$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(14,7)$	$\ge 6200460$	none	Witness	Gómez, J., Fiol, M. A., & Serra, O. (1993). On large (Δ, D)-graphs. Discrete Mathematics, 114(1-3), 219-235.
Degree-diameter problem $N(14,8)$	$\ge 65017283$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(14,9)$	$\ge 709728527$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(14,10)$	$\ge 8052187457$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(15,2)$	$\ge 190$	$\ge 183$	Witness	Dharunish Yugeswardeenoo in September 2026
Degree-diameter problem $N(15,3)$	$\ge 1620$	$\ge 812$	Witness	Mike McCormick in October 2026
Degree-diameter problem $N(15,4)$	$\ge 15552$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(15,5)$	$\ge 102060$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(15,6)$	$\ge 1428361$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(15,7)$	$\ge 9758988$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(15,8)$	$\ge 110182818$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(15,9)$	$\ge 1315254800$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(15,10)$	$\ge 16021302724$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(16,2)$	$\ge 216$	$\ge 183$	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs, orbit graphs and lifts. Zenodo.
Degree-diameter problem $N(16,3)$	$\ge 1920$	$\ge 1055$	Witness	Ryosuke Mizuno in September 2026
Degree-diameter problem $N(16,4)$	$\ge 16384$	none	Witness	J. Amarel, N. DeBardeleben, M. Grosskopf, V. Job, E. Lawrence, L. Monroe, and R. Somasundaram (LANL, using URSA) in September 2026
Degree-diameter problem $N(16,5)$	$\ge 153600$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(16,6)$	$\ge 1793786$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(16,7)$	$\ge 14995367$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(16,8)$	$\ge 185488215$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(16,9)$	$\ge 2345620783$	none	Witness	Dharunish Yugeswardeenoo in October 2026
Degree-diameter problem $N(16,10)$	$\ge 29899503497$	none	Witness	Nishant Bhakar in October 2026
Degree-diameter problem $N(17,3)$	$\ge 2210$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, orbit graphs and clique substitution. Zenodo.
Degree-diameter problem $N(17,4)$	$\ge 19121$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from generalized quadrangles and hexagons. Zenodo.
Degree-diameter problem $N(17,5)$	$\ge 153600$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(17,6)$	$\ge 3217872$	none	Witness	Loz, E., & Pineda-Villavicencio, G. (2010). New benchmarks for large-scale networks with given maximum degree and diameter. The Computer Journal, 53(7), 1092-1105.
Degree-diameter problem $N(17,7)$	$\ge 20737440$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, orbit graphs and clique substitution. Zenodo.
Degree-diameter problem $N(17,8)$	$\ge 282355100$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(17,9)$	$\ge 3970800200$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(17,10)$	$\ge 50125320600$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(18,3)$	$\ge 2210$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, orbit graphs and clique substitution. Zenodo.
Degree-diameter problem $N(18,4)$	$\ge 23956$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from generalized quadrangles and hexagons. Zenodo.
Degree-diameter problem $N(18,5)$	$\ge 197316$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs, orbit graphs and lifts. Zenodo.
Degree-diameter problem $N(18,6)$	$\ge 4022340$	none	Witness	Loz, E., & Pineda-Villavicencio, G. (2010). New benchmarks for large-scale networks with given maximum degree and diameter. The Computer Journal, 53(7), 1092-1105.
Degree-diameter problem $N(18,7)$	$\ge 29193120$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, orbit graphs and clique substitution. Zenodo.
Degree-diameter problem $N(18,8)$	$\ge 455904533$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(18,9)$	$\ge 6645271633$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(18,10)$	$\ge 90017766839$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(19,3)$	$\ge 2783$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from generalized quadrangles and hexagons. Zenodo.
Degree-diameter problem $N(19,4)$	$\ge 25050$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from generalized quadrangles and hexagons. Zenodo.
Degree-diameter problem $N(19,5)$	$\ge 222972$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs, orbit graphs and lifts. Zenodo.
Degree-diameter problem $N(19,6)$	$\ge 4024707$	none	Witness	Loz, E., & Pineda-Villavicencio, G. (2010). New benchmarks for large-scale networks with given maximum degree and diameter. The Computer Journal, 53(7), 1092-1105.
Degree-diameter problem $N(19,7)$	$\ge 41152320$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, orbit graphs and clique substitution. Zenodo.
Degree-diameter problem $N(19,8)$	$\ge 682205312$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(19,9)$	$\ge 10829019852$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(19,10)$	$\ge 120461699776$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(20,3)$	$\ge 2796$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(20,4)$	$\ge 40000$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(20,5)$	$\ge 450000$	none	Witness	Rajiv, R. (2026). Improved lower bounds for the degree-diameter problem from metacyclic groups, coset graphs and affine lifts. Zenodo.
Degree-diameter problem $N(20,6)$	$\ge 8947848$	none	Witness	Loz, E., & Pineda-Villavicencio, G. (2010). New benchmarks for large-scale networks with given maximum degree and diameter. The Computer Journal, 53(7), 1092-1105.
Degree-diameter problem $N(20,7)$	$\ge 55625185$	none	Witness	Loz, E., & Pineda-Villavicencio, G. (2010). New benchmarks for large-scale networks with given maximum degree and diameter. The Computer Journal, 53(7), 1092-1105.
Degree-diameter problem $N(20,8)$	$\ge 1051819147$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(20,9)$	$\ge 16669570133$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(20,10)$	$\ge 120461699776$	none	Witness	Rajiv, R. (2026). New lower bounds for the degree-diameter problem from Cayley graphs of metacyclic groups, slack filling and chart lifts. Zenodo.
Degree-diameter problem $N(3,2)$	$\le 10$	none	Lean proof	Table of the largest known graphs of a given diameter and maximal degree - Wikipedia
Degree-diameter problem $N(3,3)$	$\le 20$	none	Lean proof	Elspas, B. (1964, November). Topological constraints on interconnection-limited logic. In 1964 Proceedings of the Fifth Annual Symposium on Switching Circuit Theory and Logical Design (pp. 133-137). IEEE.
Degree-diameter problem $N(3,4)$	$\le 38$	none	Lean proof	Buset, D. (2000). Maximal cubic graphs with diameter 4. Discrete applied mathematics, 101(1-3), 53-61.
Degree-diameter problem $N(4,2)$	$\le 15$	none	Lean proof	Elspas, B. (1964, November). Topological constraints on interconnection-limited logic. In 1964 Proceedings of the Fifth Annual Symposium on Switching Circuit Theory and Logical Design (pp. 133-137). IEEE.
Degree-diameter problem $N(5,2)$	$\le 24$	none	Lean proof	Elspas, B. (1964, November). Topological constraints on interconnection-limited logic. In 1964 Proceedings of the Fifth Annual Symposium on Switching Circuit Theory and Logical Design (pp. 133-137). IEEE.
Degree-diameter problem $N(6,2)$	$\le 32$	none	Lean proof	Molodtsov, S. G. (2006). Largest graphs of diameter 2 and maximum degree 6. General Theory of Information Transfer and Combinatorics, 853-857.
Degree-diameter problem $N(7,2)$	$\le 50$	none	Lean proof	Table of the largest known graphs of a given diameter and maximal degree - Wikipedia

Snake-in-the-box

Constant	Literature	Verified	Evidence	Source
Snake-in-the-box $s(1)$	$\le 1$	none	Lean proof	Trivial or easy according to the secondary source.
Snake-in-the-box $s(2)$	$\le 2$	none	Lean proof	D.W. Davies, Longest "separated" paths and loops in an N cube, IEEE Transactions on Electronic Computers EC-14 (1965) 261.
Snake-in-the-box $s(3)$	$\le 4$	none	Lean proof	D.W. Davies, Longest "separated" paths and loops in an N cube, IEEE Transactions on Electronic Computers EC-14 (1965) 261.
Snake-in-the-box $s(4)$	$\le 7$	none	Lean proof	D.W. Davies, Longest "separated" paths and loops in an N cube, IEEE Transactions on Electronic Computers EC-14 (1965) 261.
Snake-in-the-box $s(5)$	$\le 13$	none	Lean proof	D.W. Davies, Longest "separated" paths and loops in an N cube, IEEE Transactions on Electronic Computers EC-14 (1965) 261.
Snake-in-the-box $s(6)$	$\le 26$	none	Lean proof	D.W. Davies, Longest "separated" paths and loops in an N cube, IEEE Transactions on Electronic Computers EC-14 (1965) 261.
Snake-in-the-box $s(7)$	$\le 50$	none	Lean proof	K.J. Kochut, Snake-in-the-box codes for dimension 7, Journal of Combinatorial Mathematics and Combinatorial Computing 20 (1996) 175-185.
Snake-in-the-box $s(8)$	$\le 98$	none	Lean proof	P.R.J. Östergård and V.H. Pettersson, Exhaustive search for snake-in-the-box codes, Graphs and Combinatorics 31 (2015) 1019-1028.

Ramsey numbers

Constant	Literature	Verified	Evidence	Source
Ramsey number $R(3,10)$	$\ge 40$	$\ge 39$	Witness	G. Exoo, On Two Classical Ramsey Numbers of the Form R(3, n), SIAM Journal on Discrete Mathematics, 2 (1989) 488-490.
Ramsey number $R(3,11)$	$\ge 47$	$\ge 46$	Witness	G. Exoo, On Some Small Classical Ramsey Numbers, Electronic Journal of Combinatorics, http://www.combinatorics.org, #P68, 20(1) (2013), 6 pages.
Ramsey number $R(3,12)$	$\ge 53$	$\ge 49$	Witness	M. Kolodyazhny, Novye Nizhnie Granitsy Chisel Ramseya R(3, 12) i R(3, 13) (in Russian), Matematicheskoye i Informacionnoe Modelirovanie, Tyumen, 14 (2015) 126-130.
Ramsey number $R(3,13)$	$\ge 61$	$\ge 58$	Witness	A. Nagda, P. Raghavan and A. Thakurta, Reinforced Generation of Combinatorial Structures: Ramsey Numbers, arXiv:2603.09172 (2026).
Ramsey number $R(3,14)$	$\ge 67$	$\ge 64$	Witness	M. Kolodyazhny, graphs available at http://aluarium.net/forum/wiki-article-17.html, personal communication (2016).
Ramsey number $R(3,15)$	$\ge 74$	$\ge 72$	Witness	M. Kolodyazhny, graphs available at http://aluarium.net/forum/wiki-article-17.html, personal communication (2016).
Ramsey number $R(4,6)$	$\ge 36$	$\ge 34$	Witness	G. Exoo, On the Ramsey Number R(4, 6), Electronic Journal of Combinatorics, http://www.combinatorics.org, #P66, 19(1) (2012), 5 pages.
Ramsey number $R(4,7)$	$\ge 49$	$\ge 47$	Witness	G. Exoo, Applying Optimization Algorithm to Ramsey Problems, in Graph Theory, Combinatorics, Algorithms, and Applications (Y. Alavi ed.), SIAM Philadelphia, (1989) 175-179.
Ramsey number $R(4,8)$	$\ge 59$	$\ge 52$	Witness	G. Exoo and M. Tatarevic, New Lower Bounds for 28 Classical Ramsey Numbers, Electronic Journal of Combinatorics, http:// www.combinatorics.org, #P3.11, 22(3) (2015), 12 pages. Graphs available at the journal site and at http://cs.indstate.edu/ge/RAMSEY/ExTa.
Ramsey number $R(4,9)$	$\ge 73$	$\ge 69$	Witness	G. Exoo, Indiana State University, personal communication (2005-2006). Constructions available at http://cs.indstate.edu/ge/RAMSEY.
Ramsey number $R(4,10)$	$\ge 92$	none	Witness	H. Harborth and S. Krause, Ramsey Numbers for Circulant Colorings, Congressus Numerantium, 161 (2003) 139-150.
Ramsey number $R(4,11)$	$\ge 102$	none	Witness	G. Exoo and M. Tatarevic, New Lower Bounds for 28 Classical Ramsey Numbers, Electronic Journal of Combinatorics, http:// www.combinatorics.org, #P3.11, 22(3) (2015), 12 pages. Graphs available at the journal site and at http://cs.indstate.edu/ge/RAMSEY/ExTa.
Ramsey number $R(4,12)$	$\ge 128$	none	Witness	Su Wenlong, Luo Haipeng and Li Qiao, New Lower Bounds of Classical Ramsey Numbers R(4, 12), R(5, 11) and R(5, 12), Chinese Science Bulletin, 43, 6 (1998) 528.
Ramsey number $R(4,13)$	$\ge 139$	none	Witness	A. Nagda, P. Raghavan and A. Thakurta, Reinforced Generation of Combinatorial Structures: Ramsey Numbers, arXiv:2603.09172 (2026).
Ramsey number $R(4,14)$	$\ge 148$	none	Witness	A. Nagda, P. Raghavan and A. Thakurta, Reinforced Generation of Combinatorial Structures: Ramsey Numbers, arXiv:2603.09172 (2026).
Ramsey number $R(4,15)$	$\ge 159$	none	Witness	A. Nagda, P. Raghavan and A. Thakurta, Reinforced Generation of Combinatorial Structures: Ramsey Numbers, arXiv:2603.09172 (2026).
Ramsey number $R(5,5)$	$\ge 43$	$\ge 42$	Witness	G. Exoo, A Lower Bound for R(5, 5), Journal of Graph Theory, 13 (1989) 97-98.
Ramsey number $R(5,6)$	$\ge 59$	$\ge 54$	Witness	G. Exoo, Indiana State University, A Lower Bound for R(5, 6), manuscript (2023).
Ramsey number $R(5,7)$	$\ge 80$	$\ge 71$	Witness	N.J. Calkin, P. Erdős and C.A. Tovey, New Ramsey Bounds from Cyclic Graphs of Prime Order, SIAM Journal on Discrete Mathematics, 10 (1997) 381-387.
Ramsey number $R(5,8)$	$\ge 101$	none	Witness	H. Harborth and S. Krause, Ramsey Numbers for Circulant Colorings, Congressus Numerantium, 161 (2003) 139-150.
Ramsey number $R(5,9)$	$\ge 133$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(5,10)$	$\ge 149$	none	Witness	G. Exoo and M. Tatarevic, New Lower Bounds for 28 Classical Ramsey Numbers, Electronic Journal of Combinatorics, http:// www.combinatorics.org, #P3.11, 22(3) (2015), 12 pages. Graphs available at the journal site and at http://cs.indstate.edu/ge/RAMSEY/ExTa.
Ramsey number $R(5,11)$	$\ge 183$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(5,12)$	$\ge 203$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(5,13)$	$\ge 233$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(5,14)$	$\ge 267$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(5,15)$	$\ge 275$	none	Witness	Trivial or easy according to the secondary source.
Ramsey number $R(6,7)$	$\ge 115$	none	Witness	G. Exoo and M. Tatarevic, New Lower Bounds for 28 Classical Ramsey Numbers, Electronic Journal of Combinatorics, http:// www.combinatorics.org, #P3.11, 22(3) (2015), 12 pages. Graphs available at the journal site and at http://cs.indstate.edu/ge/RAMSEY/ExTa.
Ramsey number $R(6,8)$	$\ge 134$	none	Witness	G. Exoo and M. Tatarevic, New Lower Bounds for 28 Classical Ramsey Numbers, Electronic Journal of Combinatorics, http:// www.combinatorics.org, #P3.11, 22(3) (2015), 12 pages. Graphs available at the journal site and at http://cs.indstate.edu/ge/RAMSEY/ExTa.
Ramsey number $R(6,9)$	$\ge 183$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(6,10)$	$\ge 204$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(6,11)$	$\ge 262$	none	Witness	M. Tatarevic, personal communication, graph constructions for lower bounds on Ramsey numbers at http://github.com/milostatarevic/ramsey-numbers/tree/master/graphs (2020).
Ramsey number $R(6,12)$	$\ge 294$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(6,13)$	$\ge 347$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(6,15)$	$\ge 401$	none	Witness	Trivial or easy according to the secondary source.
Ramsey number $R(7,8)$	$\ge 219$	none	Witness	M. Tatarevic, personal communication, graph constructions for lower bounds on Ramsey numbers at http://github.com/milostatarevic/ramsey-numbers/tree/master/graphs (2020).
Ramsey number $R(7,9)$	$\ge 252$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(7,10)$	$\ge 292$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(7,11)$	$\ge 405$	none	Witness	Xu Xiaodong, Xie Zheng, G. Exoo and S.P. Radziszowski, Constructive Lower Bounds on Classical Multicolor Ramsey Numbers, Electronic Journal of Combinatorics, http://www.combinatorics.org, #R35, 11(1) (2004), 24 pages.
Ramsey number $R(7,12)$	$\ge 417$	none	Witness	Xiaodong Xu, Zehui Shao and S.P. Radziszowski, More Constructive Lower Bounds on Classical Ramsey Numbers, SIAM Journal on Discrete Mathematics, 25 (2011) 394-400.
Ramsey number $R(7,13)$	$\ge 511$	none	Witness	Xu Xiaodong, Xie Zheng and S.P. Radziszowski, A Constructive Approach for the Lower Bounds on the Ramsey Numbers R(s, t), Journal of Graph Theory, 47 (2004) 231-239.
Ramsey number $R(8,9)$	$\ge 329$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(8,10)$	$\ge 343$	none	Witness	E. Kuznetsov, Computational Lower Limits on Small Ramsey Numbers, preprint, arXiv, http://arxiv.org/abs/1505.07186 (2016).
Ramsey number $R(8,11)$	$\ge 457$	none	Witness	Trivial or easy according to the secondary source.
Ramsey number $R(8,13)$	$\ge 817$	none	Witness	Xu Xiaodong, Xie Zheng, G. Exoo and S.P. Radziszowski, Constructive Lower Bounds on Classical Multicolor Ramsey Numbers, Electronic Journal of Combinatorics, http://www.combinatorics.org, #R35, 11(1) (2004), 24 pages.
Ramsey number $R(8,15)$	$\ge 873$	none	Witness	Trivial or easy according to the secondary source.
Ramsey number $R(9,9)$	$\ge 565$	none	Witness	R. Mathon, Lower Bounds for Ramsey Numbers and Association Schemes, Journal of Combinatorial Theory, Series B, 42 (1987) 122-127.
Ramsey number $R(9,10)$	$\ge 581$	none	Witness	Xiaodong Xu, Zehui Shao and S.P. Radziszowski, More Constructive Lower Bounds on Classical Ramsey Numbers, SIAM Journal on Discrete Mathematics, 25 (2011) 394-400.
Ramsey number $R(10,10)$	$\ge 798$	none	Witness	R. Mathon, Lower Bounds for Ramsey Numbers and Association Schemes, Journal of Combinatorial Theory, Series B, 42 (1987) 122-127.
Ramsey number $R(10,15)$	$\ge 1313$	none	Witness	Trivial or easy according to the secondary source.
Ramsey number $R(3,4)$	$\le 9$	none	Lean proof	R.E. Greenwood and A.M. Gleason, Combinatorial Relations and Chromatic Graphs, Canadian Journal of Mathematics, 7 (1955) 1-7.
Ramsey number $R(3,5)$	$\le 14$	none	Lean proof	R.E. Greenwood and A.M. Gleason, Combinatorial Relations and Chromatic Graphs, Canadian Journal of Mathematics, 7 (1955) 1-7.
Ramsey number $R(3,6)$	$\le 18$	none	Lean proof	G. Kéry, On a Theorem of Ramsey (in Hungarian), Matematikai Lapok, 15 (1964) 204-224.
Ramsey number $R(3,7)$	$\le 23$	none	Lean proof	J.E. Graver and J. Yackel, Some Graph Theoretic Results Associated with Ramsey's Theorem, Journal of Combinatorial Theory, 4 (1968) 125-175.
Ramsey number $R(3,8)$	$\le 28$	none	Lean proof	B.D. McKay and Zhang Ke Min, The Value of the Ramsey Number R(3, 8), Journal of Graph Theory, 16 (1992) 99-105.
Ramsey number $R(3,9)$	$\le 36$	none	Lean proof	C. Grinstead and S. Roberts, On the Ramsey Numbers R(3, 8) and R(3, 9), Journal of Combinatorial Theory, Series B, 33 (1982) 27-51.
Ramsey number $R(3,10)$	$\le 41$	none	Lean proof	V. Angeltveit, R(3, 10) ≤ 41, Electronic Journal of Combinatorics 32(4) (2025) #P4.30.
Ramsey number $R(3,11)$	$\le 50$	none	Lean proof	J. Goedgebeur and S.P. Radziszowski, New Computational Upper Bounds for Ramsey Numbers R(3, k), Electronic Journal of Combinatorics, http://www.combinatorics.org, #P30, 20(1) (2013), 28 pages.
Ramsey number $R(3,12)$	$\le 59$	none	Lean proof	A. Lesser, Theoretical and Computational Aspects of Ramsey Theory, Examensarbeten i Matematik, Matematiska Institutionen, Stockholms Universitet, 3, http://www2.math.su.se/gemensamt/grund/exjobb/matte/2001 (2001).
Ramsey number $R(3,13)$	$\le 68$	none	Lean proof	J. Goedgebeur and S.P. Radziszowski, New Computational Upper Bounds for Ramsey Numbers R(3, k), Electronic Journal of Combinatorics, http://www.combinatorics.org, #P30, 20(1) (2013), 28 pages.
Ramsey number $R(3,14)$	$\le 77$	none	Lean proof	J. Goedgebeur and S.P. Radziszowski, New Computational Upper Bounds for Ramsey Numbers R(3, k), Electronic Journal of Combinatorics, http://www.combinatorics.org, #P30, 20(1) (2013), 28 pages.
Ramsey number $R(3,15)$	$\le 87$	none	Lean proof	J. Goedgebeur and S.P. Radziszowski, New Computational Upper Bounds for Ramsey Numbers R(3, k), Electronic Journal of Combinatorics, http://www.combinatorics.org, #P30, 20(1) (2013), 28 pages.
Ramsey number $R(4,4)$	$\le 18$	none	Lean proof	R.E. Greenwood and A.M. Gleason, Combinatorial Relations and Chromatic Graphs, Canadian Journal of Mathematics, 7 (1955) 1-7.
Ramsey number $R(4,5)$	$\le 25$	none	Lean proof	B.D. McKay and S.P. Radziszowski, R(4, 5) = 25, Journal of Graph Theory, 19 (1995) 309-322.
Ramsey number $R(4,6)$	$\le 40$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(4,7)$	$\le 58$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(4,8)$	$\le 79$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(4,9)$	$\le 105$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(4,10)$	$\le 135$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(4,11)$	$\le 170$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(4,12)$	$\le 210$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(4,13)$	$\le 256$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(4,14)$	$\le 307$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(4,15)$	$\le 364$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(5,5)$	$\le 46$	none	Lean proof	V. Angeltveit and B.D. McKay, R(5,5) ≤ 46, Journal of Graph Theory (2026), arXiv:2409.15709.
Ramsey number $R(5,6)$	$\le 85$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(5,7)$	$\le 133$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(5,8)$	$\le 193$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(5,9)$	$\le 282$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(5,10)$	$\le 381$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(5,11)$	$\le 511$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(5,12)$	$\le 672$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(5,13)$	$\le 860$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(5,14)$	$\le 1081$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(5,15)$	$\le 1341$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(6,6)$	$\le 160$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(6,7)$	$\le 270$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(6,8)$	$\le 423$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(6,9)$	$\le 651$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(6,10)$	$\le 944$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(6,11)$	$\le 1346$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(6,12)$	$\le 1855$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(6,13)$	$\le 2499$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(6,14)$	$\le 3301$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(6,15)$	$\le 4305$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(7,7)$	$\le 492$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(7,8)$	$\le 832$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(7,9)$	$\le 1368$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(7,10)$	$\le 2119$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(7,11)$	$\le 3197$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(7,12)$	$\le 4665$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(7,13)$	$\le 6653$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(7,14)$	$\le 9260$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(7,15)$	$\le 12635$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(8,8)$	$\le 1518$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(8,9)$	$\le 2662$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(8,10)$	$\le 4402$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(8,11)$	$\le 7040$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(8,12)$	$\le 10836$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(8,13)$	$\le 27485$	none	Lean proof	Huang Yi Ru, Wang Yuandi, Sheng Wancheng, Yang Jiansheng, Zhang Ke Min and Huang Jian, New Upper Bound Formulas with Parameters for Ramsey Numbers, Discrete Mathematics, 307 (2007) 760-763.
Ramsey number $R(8,14)$	$\le 41525$	none	Lean proof	Huang Yi Ru, Wang Yuandi, Sheng Wancheng, Yang Jiansheng, Zhang Ke Min and Huang Jian, New Upper Bound Formulas with Parameters for Ramsey Numbers, Discrete Mathematics, 307 (2007) 760-763.
Ramsey number $R(8,15)$	$\le 63609$	none	Lean proof	Huang Yi Ru, Wang Yuandi, Sheng Wancheng, Yang Jiansheng, Zhang Ke Min and Huang Jian, New Upper Bound Formulas with Parameters for Ramsey Numbers, Discrete Mathematics, 307 (2007) 760-763.
Ramsey number $R(9,9)$	$\le 4956$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(9,10)$	$\le 8675$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(9,11)$	$\le 14631$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(9,12)$	$\le 38832$	none	Lean proof	Huang Yi Ru, Wang Yuandi, Sheng Wancheng, Yang Jiansheng, Zhang Ke Min and Huang Jian, New Upper Bound Formulas with Parameters for Ramsey Numbers, Discrete Mathematics, 307 (2007) 760-763.
Ramsey number $R(9,13)$	$\le 64864$	none	Lean proof	Huang Yi Ru, Wang Yuandi, Sheng Wancheng, Yang Jiansheng, Zhang Ke Min and Huang Jian, New Upper Bound Formulas with Parameters for Ramsey Numbers, Discrete Mathematics, 307 (2007) 760-763.
Ramsey number $R(10,10)$	$\le 16064$	none	Lean proof	V. Angeltveit and B.D. McKay, personal communication (2019-2024).
Ramsey number $R(10,11)$	$\le 45881$	none	Lean proof	Huang Yi Ru, Wang Yuandi, Sheng Wancheng, Yang Jiansheng, Zhang Ke Min and Huang Jian, New Upper Bound Formulas with Parameters for Ramsey Numbers, Discrete Mathematics, 307 (2007) 760-763.
Ramsey number $R(10,12)$	$\le 81123$	none	Lean proof	Huang Yi Ru, Wang Yuandi, Sheng Wancheng, Yang Jiansheng, Zhang Ke Min and Huang Jian, New Upper Bound Formulas with Parameters for Ramsey Numbers, Discrete Mathematics, 307 (2007) 760-763.

Schur numbers

Constant	Literature	Verified	Evidence	Source
Schur number $S(9)$	$\ge 17803$	none	Witness	R. Ageron, P. Casteras, T. Pellerin, Y. Portella, A. Rimmel and J. Tomasik, New lower bounds for Schur and weak Schur numbers, arXiv:2112.03175.
Schur number $S(1)$	$\le 1$	none	Lean proof	Trivial or easy according to the secondary source.
Schur number $S(2)$	$\le 4$	none	Lean proof	Trivial or easy according to the secondary source.
Schur number $S(3)$	$\le 13$	none	Lean proof	Trivial or easy according to the secondary source.
Schur number $S(4)$	$\le 44$	none	Lean proof	S.W. Golomb and L.D. Baumert, Backtrack Programming, Journal of the ACM 12 (1965) 516-524.
Schur number $S(5)$	$\le 160$	none	Lean proof	M.J.H. Heule, Schur Number Five, Proceedings of the AAAI Conference on Artificial Intelligence 32 (2018) 6598-6606, arXiv:1711.08076.

Van der Waerden numbers

Constant	Literature	Verified	Evidence	Source
Van der Waerden number $W(3,5)$	$\ge 2174$	none	Witness	Rabung, J., & Lotts, M. (2012). Improving the use of cyclic zippers in finding lower bounds for van der Waerden numbers. the electronic journal of combinatorics, P35-P35.
Van der Waerden number $W(3,6)$	$\ge 11192$	none	Witness	Rabung, J., & Lotts, M. (2012). Improving the use of cyclic zippers in finding lower bounds for van der Waerden numbers. the electronic journal of combinatorics, P35-P35.
Van der Waerden number $W(3,7)$	$\ge 48812$	none	Witness	Rabung, J., & Lotts, M. (2012). Improving the use of cyclic zippers in finding lower bounds for van der Waerden numbers. the electronic journal of combinatorics, P35-P35.
Van der Waerden number $W(3,9)$	$\ge 932746$	none	Witness	Rabung, J., & Lotts, M. (2012). Improving the use of cyclic zippers in finding lower bounds for van der Waerden numbers. the electronic journal of combinatorics, P35-P35.
Van der Waerden number $W(3,10)$	$\ge 4173725$	none	Witness	Rabung, J., & Lotts, M. (2012). Improving the use of cyclic zippers in finding lower bounds for van der Waerden numbers. the electronic journal of combinatorics, P35-P35.
Van der Waerden number $W(3,11)$	$\ge 18603732$	none	Witness	Rabung, J., & Lotts, M. (2012). Improving the use of cyclic zippers in finding lower bounds for van der Waerden numbers. the electronic journal of combinatorics, P35-P35.
Van der Waerden number $W(4,6)$	$\ge 157349$	none	Witness	Monroe, D. (2022). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v7.
Van der Waerden number $W(4,7)$	$\ge 2284752$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(4,8)$	$\ge 12288156$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(4,9)$	$\ge 139847086$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(4,10)$	$\ge 1189640579$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(4,11)$	$\ge 3464368084$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(5,3)$	$\ge 171$	none	Witness	Rabung, J., & Lotts, M. (2012). Improving the use of cyclic zippers in finding lower bounds for van der Waerden numbers. the electronic journal of combinatorics, P35-P35.
Van der Waerden number $W(5,5)$	$\ge 98742$	none	Witness	Komkov, M. (2016). viXra:1611.0385.
Van der Waerden number $W(5,6)$	$\ge 786741$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(5,7)$	$\ge 15993258$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(5,8)$	$\ge 86017086$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(5,9)$	$\ge 978929596$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(5,10)$	$\ge 8327484047$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(5,11)$	$\ge 38108048914$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(6,3)$	$\ge 226$	none	Witness	Blankenship, T., Cummings, J., & Taranchuk, V. (2018). A new lower bound for van der Waerden numbers. European Journal of Combinatorics, 69, 163-168.
Van der Waerden number $W(6,5)$	$\ge 98755$	none	Witness	Komkov, M. (2016). viXra:1611.0385.
Van der Waerden number $W(6,6)$	$\ge 1555550$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(6,7)$	$\ge 111952800$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(6,8)$	$\ge 602119596$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(6,9)$	$\ge 6852507166$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(6,10)$	$\ge 58292388323$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(6,11)$	$\ge 419188538044$	none	Witness	Monroe, D. (2019). New Lower Bounds for van der Waerden Numbers Using Distributed Computing. arXiv preprint arXiv:1603.03301v6.
Van der Waerden number $W(2,3)$	$\le 9$	none	Lean proof	Chvátal, V. (1970). Some unknown van der Waerden numbers. Combinatorial structures and their applications, 31-33.
Van der Waerden number $W(2,4)$	$\le 35$	none	Lean proof	Chvátal, V. (1970). Some unknown van der Waerden numbers. Combinatorial structures and their applications, 31-33.
Van der Waerden number $W(2,5)$	$\le 178$	none	Lean proof	Stevens, R. S., & Shantaram, R. (1978). Computer-generated van der Waerden partitions. Mathematics of Computation, 32(142), 635-636.
Van der Waerden number $W(2,6)$	$\le 1132$	none	Lean proof	Kouril, M., & Paul, J. L. (2008). The van der Waerden number W (2, 6) is 1132. Experimental Mathematics, 17(1), 53-61.
Van der Waerden number $W(3,3)$	$\le 27$	none	Lean proof	Chvátal, V. (1970). Some unknown van der Waerden numbers. Combinatorial structures and their applications, 31-33.
Van der Waerden number $W(3,4)$	$\le 293$	none	Lean proof	Kouril, Michal (2012). Computing the van der Waerden number W(3,4)=293. Integers. 12: A46.
Van der Waerden number $W(4,3)$	$\le 76$	none	Lean proof	Beeler, M. D., & O'neil, P. E. (1979). Some new van der Waerden numbers. Discrete Mathematics, 28(2), 135-146.

Weak Schur numbers

Constant	Literature	Verified	Evidence	Source
Weak Schur number $WS(7)$	$\ge 2146$	none	Witness	F. Rowley, New lower bounds for weak Schur partitions, Integers 21 (2021) #A59, arXiv:2011.11292.
Weak Schur number $WS(8)$	$\ge 6976$	none	Witness	F. Rowley, New lower bounds for weak Schur partitions, Integers 21 (2021) #A59, arXiv:2011.11292.
Weak Schur number $WS(9)$	$\ge 22536$	none	Witness	R. Ageron, P. Casteras, T. Pellerin, Y. Portella, A. Rimmel and J. Tomasik, New lower bounds for Schur and weak Schur numbers, arXiv:2112.03175.
Weak Schur number $WS(1)$	$\le 2$	none	Lean proof	Trivial or easy according to the secondary source.
Weak Schur number $WS(2)$	$\le 8$	none	Lean proof	Trivial or easy according to the secondary source.
Weak Schur number $WS(3)$	$\le 23$	none	Lean proof	P.F. Blanchard, F. Harary and R. Reis, Partitions into sum-free sets, Integers 6 (2006) #A7.
Weak Schur number $WS(4)$	$\le 66$	none	Lean proof	P.F. Blanchard, F. Harary and R. Reis, Partitions into sum-free sets, Integers 6 (2006) #A7.

Arrangements of lines in the affine plane

Constant	Literature	Verified	Evidence	Source
Arrangements of $7$ lines in the affine plane	$\ge 37830$	none	Witness	L. Finschi, A Graph Theoretical Approach for Reconstruction and Generation of Oriented Matroids, Dissertation, ETH Zürich, 2001.
Arrangements of $1$ lines in the affine plane	$\le 1$	none	Lean proof	Number of ways of arranging n lines in the (affine) plane. - OEIS
Arrangements of $2$ lines in the affine plane	$\le 2$	none	Lean proof	Number of ways of arranging n lines in the (affine) plane. - OEIS
Arrangements of $3$ lines in the affine plane	$\le 4$	none	Lean proof	Number of ways of arranging n lines in the (affine) plane. - OEIS
Arrangements of $4$ lines in the affine plane	$\le 9$	none	Lean proof	Number of ways of arranging n lines in the (affine) plane. - OEIS
Arrangements of $5$ lines in the affine plane	$\le 47$	none	Lean proof	L. Finschi, A Graph Theoretical Approach for Reconstruction and Generation of Oriented Matroids, Dissertation, ETH Zürich, 2001.
Arrangements of $6$ lines in the affine plane	$\le 791$	none	Lean proof	L. Finschi, A Graph Theoretical Approach for Reconstruction and Generation of Oriented Matroids, Dissertation, ETH Zürich, 2001.
Arrangements of $7$ lines in the affine plane	$\le 37830$	none	Lean proof	L. Finschi, A Graph Theoretical Approach for Reconstruction and Generation of Oriented Matroids, Dissertation, ETH Zürich, 2001.
Arrangements of $8$ lines in the affine plane	$\le 4134940$	none	Lean proof	L. Finschi, A Graph Theoretical Approach for Reconstruction and Generation of Oriented Matroids, Dissertation, ETH Zürich, 2001.

Arrangements of lines in general position

Constant	Literature	Verified	Evidence	Source
Arrangements of $8$ lines in general position	$\ge 38609$	none	Witness	Number of ways of arranging n straight lines in general position in the (affine) plane. - OEIS
Arrangements of $9$ lines in general position	$\ge 3111341$	none	Witness	T. Christ, Discrete Descriptions of Geometric Objects, Dissertation, ETH Zürich, 2011, with the Database of Combinatorially Different Simple Line Arrangements.
Arrangements of $1$ lines in general position	$\le 1$	none	Lean proof	Number of ways of arranging n straight lines in general position in the (affine) plane. - OEIS
Arrangements of $2$ lines in general position	$\le 1$	none	Lean proof	Number of ways of arranging n straight lines in general position in the (affine) plane. - OEIS
Arrangements of $3$ lines in general position	$\le 1$	none	Lean proof	Number of ways of arranging n straight lines in general position in the (affine) plane. - OEIS
Arrangements of $4$ lines in general position	$\le 1$	none	Lean proof	Number of ways of arranging n straight lines in general position in the (affine) plane. - OEIS
Arrangements of $5$ lines in general position	$\le 6$	none	Lean proof	G. Ringel, Teilungen der Ebene durch Geraden oder topologische Geraden, Mathematische Zeitschrift 64 (1956) 79-102.
Arrangements of $6$ lines in general position	$\le 43$	none	Lean proof	G. Ringel, Teilungen der Ebene durch Geraden oder topologische Geraden, Mathematische Zeitschrift 64 (1956) 79-102.
Arrangements of $7$ lines in general position	$\le 922$	none	Lean proof	G. Ringel, Teilungen der Ebene durch Geraden oder topologische Geraden, Mathematische Zeitschrift 64 (1956) 79-102.
Arrangements of $8$ lines in general position	$\le 38609$	none	Lean proof	Number of ways of arranging n straight lines in general position in the (affine) plane. - OEIS
Arrangements of $9$ lines in general position	$\le 3111341$	none	Lean proof	T. Christ, Discrete Descriptions of Geometric Objects, Dissertation, ETH Zürich, 2011, with the Database of Combinatorially Different Simple Line Arrangements.

Circle packing in an equilateral triangle

Constant	Literature	Verified	Evidence	Source
Packing $7$ unit circles in an equilateral triangle	$\ge 2+4\sqrt{3}$	none	Lean proof	Melissen, H. (1993). Densest packings of congruent circles in an equilateral triangle. The American Mathematical Monthly, 100(10), 916-925.
Packing $8$ unit circles in an equilateral triangle	$\ge 2+2\sqrt{3}+\frac{2\sqrt{33}}{3}$	none	Lean proof	Melissen, H. (1993). Densest packings of congruent circles in an equilateral triangle. The American Mathematical Monthly, 100(10), 916-925.
Packing $9$ unit circles in an equilateral triangle	$\ge 6+2\sqrt{3}$	none	Lean proof	Melissen, H. (1993). Densest packings of congruent circles in an equilateral triangle. The American Mathematical Monthly, 100(10), 916-925.
Packing $11$ unit circles in an equilateral triangle	$\ge 4+2\sqrt{3}+\frac{4\sqrt{6}}{3}$	none	Lean proof	Melissen, J. B. M. (1994). Optimal packings of eleven equal circles in an equilateral triangle. Acta Mathematica Hungarica, 65(4), 389-393.
Packing $12$ unit circles in an equilateral triangle	$\ge 4+4\sqrt{3}$	none	Lean proof	Melissen in 1994
Packing $14$ unit circles in an equilateral triangle	$\ge 8+2\sqrt{3}$	none	Lean proof	Payan, C. (1997). Empilement de cercles égaux dans un triangle équilatéral. À propos d'une conjecture d'Erdős-Oler. Discrete Mathematics, 165-166, 555-565.
Packing $15$ unit circles in an equilateral triangle	$\ge 8+2\sqrt{3}$	none	Lean proof	Groemer, H. (1960). Über die Einlagerung von Kreisen in einen konvexen Bereich. Math. Z., 73, 285-294; Oler, N. (1961). A finite packing problem. Canad. Math. Bull., 4, 153-155.

Kissing numbers

Constant	Literature	Verified	Evidence	Source
Kissing number for $\mathbb{R}^{9}$	$\ge 306$	$\ge 272$	Witness	J. Leech and N.J.A. Sloane, Sphere packings and error-correcting codes, Canadian Journal of Mathematics 23 (1971) 718-745.
Kissing number for $\mathbb{R}^{10}$	$\ge 510$	$\ge 336$	Witness	M. Ganzhinov, Highly symmetric lines, Linear Algebra and its Applications 722 (2025) 12-37, arXiv:2207.08266.
Kissing number for $\mathbb{R}^{11}$	$\ge 604$	$\ge 438$	Witness	F. Bianchi, Y. Kwon, A. Pappu, and J. Zou, Harnessing the Collective Intelligence of AI Agents in the Wild for New Discoveries, arXiv:2606.10402.
Kissing number for $\mathbb{R}^{12}$	$\ge 841$	$\ge 756$	Witness	R. Takhanov, Z. Assylbekov, and S. Yun, Structure of kissing arrangements in R^12 and a place for the 841st sphere, arXiv:2606.18984.
Kissing number for $\mathbb{R}^{13}$	$\ge 1154$	$\ge 906$	Witness	V.A. Zinoviev and T. Ericson, New lower bounds for contact numbers in small dimensions, Problems of Information Transmission 35 (1999) 287-294.
Kissing number for $\mathbb{R}^{14}$	$\ge 1932$	$\ge 1422$	Witness	M. Ganzhinov, Highly symmetric lines, Linear Algebra and its Applications 722 (2025) 12-37, arXiv:2207.08266.
Kissing number for $\mathbb{R}^{15}$	$\ge 2564$	$\ge 2340$	Witness	J. Leech and N.J.A. Sloane, Sphere packings and error-correcting codes, Canadian Journal of Mathematics 23 (1971) 718-745.
Kissing number for $\mathbb{R}^{17}$	$\ge 5730$	$\ge 5346$	Witness	H. Cohn and A. Li, Improved kissing numbers in seventeen through twenty-one dimensions, arXiv:2411.04916.
Kissing number for $\mathbb{R}^{18}$	$\ge 8358$	$\ge 7398$	Witness	A. Kravatskiy, KissingNumbers (GitHub repository), 2026.
Kissing number for $\mathbb{R}^{19}$	$\ge 12460$	$\ge 10668$	Witness	K. Li, Improved Kissing Numbers in Nineteen and Twenty-One Dimensions, Hexagon hexagon:2610.00248.
Kissing number for $\mathbb{R}^{20}$	$\ge 19448$	$\ge 17400$	Witness	H. Cohn and A. Li, Improved kissing numbers in seventeen through twenty-one dimensions, arXiv:2411.04916.
Kissing number for $\mathbb{R}^{21}$	$\ge 31560$	$\ge 27720$	Witness	K. Li, Improved Kissing Numbers in Nineteen and Twenty-One Dimensions, Hexagon hexagon:2610.00248.
Kissing number for $\mathbb{R}^{1}$	$\le 2$	none	Lean proof	Trivial or easy according to the secondary source.
Kissing number for $\mathbb{R}^{2}$	$\le 6$	none	Lean proof	Trivial or easy according to the secondary source.
Kissing number for $\mathbb{R}^{3}$	$\le 12$	none	Lean proof	K. Schütte and B.L. van der Waerden, Das Problem der dreizehn Kugeln, Mathematische Annalen 125 (1953) 325-334.
Kissing number for $\mathbb{R}^{4}$	$\le 24$	none	Lean proof	O.R. Musin, The kissing number in four dimensions, Annals of Mathematics 168 (2008) 1-32, arXiv:math/0309430.
Kissing number for $\mathbb{R}^{5}$	$\le 44$	none	Lean proof	H.D. Mittelmann and F. Vallentin, High accuracy semidefinite programming bounds for kissing numbers, Experimental Mathematics 19 (2010) 174-178, arXiv:0902.1105.
Kissing number for $\mathbb{R}^{6}$	$\le 77$	none	Lean proof	D. de Laat, N.M. Leijenhorst, and W.H.H. de Muinck Keizer, Optimality and uniqueness of the D4 root system, arXiv:2404.18794.
Kissing number for $\mathbb{R}^{7}$	$\le 134$	none	Lean proof	H.D. Mittelmann and F. Vallentin, High accuracy semidefinite programming bounds for kissing numbers, Experimental Mathematics 19 (2010) 174-178, arXiv:0902.1105.
Kissing number for $\mathbb{R}^{8}$	$\le 240$	none	Lean proof	A.M. Odlyzko and N.J.A. Sloane, New bounds on the number of unit spheres that can touch a unit sphere in n dimensions, Journal of Combinatorial Theory, Series A 26 (1979) 210-214.
Kissing number for $\mathbb{R}^{9}$	$\le 363$	none	Lean proof	F.C. Machado and F.M. de Oliveira Filho, Improving the semidefinite programming bound for the kissing number by exploiting polynomial symmetry, Experimental Mathematics 27 (2018) 362-369.
Kissing number for $\mathbb{R}^{10}$	$\le 553$	none	Lean proof	F.C. Machado and F.M. de Oliveira Filho, Improving the semidefinite programming bound for the kissing number by exploiting polynomial symmetry, Experimental Mathematics 27 (2018) 362-369.
Kissing number for $\mathbb{R}^{11}$	$\le 868$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{12}$	$\le 1355$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{13}$	$\le 2064$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{14}$	$\le 3174$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{15}$	$\le 4853$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{16}$	$\le 7320$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{17}$	$\le 10978$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{18}$	$\le 16406$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{19}$	$\le 24417$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{20}$	$\le 36195$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{21}$	$\le 53524$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{22}$	$\le 80810$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{23}$	$\le 122351$	none	Lean proof	N. Leijenhorst and D. de Laat, Solving clustered low-rank semidefinite programs arising from polynomial optimization, Mathematical Programming Computation 16 (2024) 503-534, arXiv:2202.12077.
Kissing number for $\mathbb{R}^{24}$	$\le 196560$	none	Lean proof	A.M. Odlyzko and N.J.A. Sloane, New bounds on the number of unit spheres that can touch a unit sphere in n dimensions, Journal of Combinatorial Theory, Series A 26 (1979) 210-214.

Packing unit squares in a square

Constant	Literature	Verified	Evidence	Source
Packing unit squares in a square $s(2)$	$\ge 2$	$\ge \sqrt{2}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(3)$	$\ge 2$	$\ge \sqrt{3}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(5)$	$\ge 2 + \frac{1}{\sqrt{2}}$	$\ge \sqrt{5}$	Lean proof	F. Göbel, Geometrical Packing and Covering Problems, in Packing and Covering in Combinatorics, A. Schrijver (ed.), Math Centrum Tracts 106 (1979) 179-199.
Packing unit squares in a square $s(5)$	$\le 2 + \frac{1}{\sqrt{2}}$	$\le 3$	Lean proof	F. Göbel, Geometrical Packing and Covering Problems, in Packing and Covering in Combinatorics, A. Schrijver (ed.), Math Centrum Tracts 106 (1979) 179-199.
Packing unit squares in a square $s(6)$	$\ge 3$	$\ge \sqrt{6}$	Lean proof	Kearney, M. J., & Shiu, P. (2002). Efficient packing of unit squares in a square. The Electronic Journal of Combinatorics, 9, R14.
Packing unit squares in a square $s(7)$	$\ge 3$	$\ge \sqrt{7}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(8)$	$\ge 3$	$\ge \sqrt{8}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(10)$	$\ge 3 + \frac{1}{\sqrt{2}}$	$\ge \sqrt{10}$	Lean proof	Stromquist, W. (2003). Packing 10 or 11 unit squares in a square. The Electronic Journal of Combinatorics, 10, R8.
Packing unit squares in a square $s(10)$	$\le 3 + \frac{1}{\sqrt{2}}$	$\le 4$	Lean proof	F. Göbel, Geometrical Packing and Covering Problems, in Packing and Covering in Combinatorics, A. Schrijver (ed.), Math Centrum Tracts 106 (1979) 179-199.
Packing unit squares in a square $s(11)$	$\ge 2 + \frac{4}{\sqrt{5}}$	$\ge \sqrt{11}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(11)$	$\le {\approx}3.8771$	$\le 4$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(12)$	$\ge 2 + \frac{4}{\sqrt{5}}$	$\ge \sqrt{12}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(13)$	$\ge 4$	$\ge \sqrt{13}$	Lean proof	Bentz, W. (2010). Optimal packings of 13 and 46 unit squares in a square. The Electronic Journal of Combinatorics, 17, R126.
Packing unit squares in a square $s(14)$	$\ge 4$	$\ge \sqrt{14}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(15)$	$\ge 4$	$\ge \sqrt{15}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(17)$	$\ge \frac{40\sqrt{2}+19}{17}$	$\ge \sqrt{17}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(17)$	$\le {\approx}4.6755$	$\le 5$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(18)$	$\ge \frac{40\sqrt{2}+19}{17}$	$\ge \sqrt{18}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(18)$	$\le \frac{7+\sqrt{7}}{2}$	$\le 5$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(19)$	$\ge 6\sqrt{2}-4$	$\ge \sqrt{19}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(19)$	$\le 3+\frac{4\sqrt{2}}{3}$	$\le 5$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(20)$	$\ge 6\sqrt{2}-4$	$\ge \sqrt{20}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(21)$	$\ge 4.7438$	$\ge \sqrt{21}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(22)$	$\ge 5$	$\ge \sqrt{22}$	Lean proof	Bentz, W. (2016). Optimal packings of 22 and 33 unit squares in a square. arXiv preprint arXiv:1606.03746.
Packing unit squares in a square $s(23)$	$\ge 5$	$\ge \sqrt{23}$	Lean proof	Nagamochi, H. (2005). Packing unit squares in a rectangle. The Electronic Journal of Combinatorics, 12, R37.
Packing unit squares in a square $s(24)$	$\ge 5$	$\ge \sqrt{24}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(26)$	$\ge 2\sqrt{2}+\frac{27+2\sqrt{10}}{13}$	$\ge \sqrt{26}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(26)$	$\le \frac{7}{2}+\frac{3\sqrt{2}}{2}$	$\le 6$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(27)$	$\ge 2\sqrt{2}+\frac{27+2\sqrt{10}}{13}$	$\ge \sqrt{27}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(27)$	$\le 5+\frac{1}{\sqrt{2}}$	$\le 6$	Lean proof	F. Göbel, Geometrical Packing and Covering Problems, in Packing and Covering in Combinatorics, A. Schrijver (ed.), Math Centrum Tracts 106 (1979) 179-199.
Packing unit squares in a square $s(28)$	$\ge 2\sqrt{2}+\frac{6}{\sqrt{5}}$	$\ge \sqrt{28}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(28)$	$\le {\approx}5.8244$	$\le 6$	Lean proof	David Ellsworth in December 2025
Packing unit squares in a square $s(29)$	$\ge 2\sqrt{2}+\frac{6}{\sqrt{5}}$	$\ge \sqrt{29}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(29)$	$\le {\approx}5.9338$	$\le 6$	Lean proof	Thomas Schadt in December 2025 (optimized by David Ellsworth)
Packing unit squares in a square $s(30)$	$\ge 2\sqrt{2}+\frac{6}{\sqrt{5}}$	$\ge \sqrt{30}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(31)$	$\ge 5.6415$	$\ge \sqrt{31}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(33)$	$\ge 6$	$\ge \sqrt{33}$	Lean proof	Bentz, W. (2016). Optimal packings of 22 and 33 unit squares in a square. arXiv preprint arXiv:1606.03746.
Packing unit squares in a square $s(34)$	$\ge 6$	$\ge \sqrt{34}$	Lean proof	Nagamochi, H. (2005). Packing unit squares in a rectangle. The Electronic Journal of Combinatorics, 12, R37.
Packing unit squares in a square $s(35)$	$\ge 6$	$\ge \sqrt{35}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(37)$	$\ge 2\sqrt{2}+\frac{113+10\sqrt{3}}{37}$	$\ge \sqrt{37}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(37)$	$\le {\approx}6.5986$	$\le 7$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(38)$	$\ge 2\sqrt{2}+\frac{113+10\sqrt{3}}{37}$	$\ge \sqrt{38}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(38)$	$\le 6+\frac{1}{\sqrt{2}}$	$\le 7$	Lean proof	F. Göbel, Geometrical Packing and Covering Problems, in Packing and Covering in Combinatorics, A. Schrijver (ed.), Math Centrum Tracts 106 (1979) 179-199.
Packing unit squares in a square $s(39)$	$\ge 2\sqrt{2}+\frac{113+10\sqrt{3}}{37}$	$\ge \sqrt{39}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(39)$	$\le {\approx}6.8107$	$\le 7$	Lean proof	Thomas Schadt in January 2026 (refined and optimized by David Ellsworth)
Packing unit squares in a square $s(40)$	$\ge 2\sqrt{2}+\frac{8}{\sqrt{5}}$	$\ge \sqrt{40}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(40)$	$\le 4+2\sqrt{2}$	$\le 7$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(41)$	$\ge 2\sqrt{2}+\frac{8}{\sqrt{5}}$	$\ge \sqrt{41}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(41)$	$\le {\approx}6.9267$	$\le 7$	Lean proof	Thomas Schadt in December 2025 (optimized by David Ellsworth)
Packing unit squares in a square $s(46)$	$\ge 7$	$\ge \sqrt{46}$	Lean proof	Bentz, W. (2010). Optimal packings of 13 and 46 unit squares in a square. The Electronic Journal of Combinatorics, 17, R126.
Packing unit squares in a square $s(47)$	$\ge 7$	$\ge \sqrt{47}$	Lean proof	Nagamochi, H. (2005). Packing unit squares in a rectangle. The Electronic Journal of Combinatorics, 12, R37.
Packing unit squares in a square $s(48)$	$\ge 7$	$\ge \sqrt{48}$	Lean proof	Nagamochi, H. (2005). Packing unit squares in a rectangle. The Electronic Journal of Combinatorics, 12, R37.
Packing unit squares in a square $s(50)$	$\ge 2\sqrt{2}+\frac{101+3\sqrt{14}}{25}$	$\ge \sqrt{50}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(50)$	$\le 7+\frac{4}{7}$	$\le 8$	Lean proof	Thomas Schadt in December 2025 (optimized by David Ellsworth)
Packing unit squares in a square $s(51)$	$\ge 2\sqrt{2}+\frac{101+3\sqrt{14}}{25}$	$\ge \sqrt{51}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(51)$	$\le {\approx}7.7008$	$\le 8$	Lean proof	Thomas Schadt in January 2026 (refined and optimized by David Ellsworth)
Packing unit squares in a square $s(52)$	$\ge 2\sqrt{2}+\frac{101+3\sqrt{14}}{25}$	$\ge \sqrt{52}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(52)$	$\le 7+\frac{1}{\sqrt{2}}$	$\le 8$	Lean proof	F. Göbel, Geometrical Packing and Covering Problems, in Packing and Covering in Combinatorics, A. Schrijver (ed.), Math Centrum Tracts 106 (1979) 179-199.
Packing unit squares in a square $s(53)$	$\ge 2\sqrt{2}+\frac{101+3\sqrt{14}}{25}$	$\ge \sqrt{53}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(53)$	$\le \frac{13}{2}+\frac{\sqrt{7}}{2}$	$\le 8$	Lean proof	David Ellsworth in February 2026
Packing unit squares in a square $s(54)$	$\le 7-\frac{\sqrt{2}}{2}+\sqrt{1+\sqrt{2}}$	$\le 8$	Lean proof	Joe DeVincentis in April 2014
Packing unit squares in a square $s(55)$	$\le {\approx}7.9458$	$\le 8$	Lean proof	David Ellsworth in February 2026
Packing unit squares in a square $s(62)$	$\ge 8$	$\ge \sqrt{62}$	Lean proof	Nagamochi, H. (2005). Packing unit squares in a rectangle. The Electronic Journal of Combinatorics, 12, R37.
Packing unit squares in a square $s(63)$	$\ge 8$	$\ge \sqrt{63}$	Lean proof	Nagamochi, H. (2005). Packing unit squares in a rectangle. The Electronic Journal of Combinatorics, 12, R37.
Packing unit squares in a square $s(65)$	$\ge 2\sqrt{2}+\frac{71}{13}$	$\ge \sqrt{65}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(65)$	$\le 5+\frac{5}{\sqrt{2}}$	$\le 9$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(66)$	$\ge 2\sqrt{2}+\frac{71}{13}$	$\ge \sqrt{66}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(66)$	$\le 3+4\sqrt{2}$	$\le 9$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(67)$	$\ge 2\sqrt{2}+\frac{71}{13}$	$\ge \sqrt{67}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(67)$	$\le 8+\frac{1}{\sqrt{2}}$	$\le 9$	Lean proof	F. Göbel, Geometrical Packing and Covering Problems, in Packing and Covering in Combinatorics, A. Schrijver (ed.), Math Centrum Tracts 106 (1979) 179-199.
Packing unit squares in a square $s(68)$	$\ge 2\sqrt{2}+\frac{71}{13}$	$\ge \sqrt{68}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(68)$	$\le {\approx}8.7988$	$\le 9$	Lean proof	Jake Loyd in September 2026
Packing unit squares in a square $s(69)$	$\le {\approx}8.8272$	$\le 9$	Lean proof	hmbelvedere in July 2026 (refound and optimized by David Ellsworth in September 2026)
Packing unit squares in a square $s(70)$	$\le {\approx}8.8817$	$\le 9$	Lean proof	Joe DeVincentis in April 2014
Packing unit squares in a square $s(71)$	$\le {\approx}8.9441$	$\le 9$	Lean proof	Thomas Schadt in December 2025 (optimized by David Ellsworth)
Packing unit squares in a square $s(79)$	$\ge 9$	$\ge \sqrt{79}$	Lean proof	Nagamochi, H. (2005). Packing unit squares in a rectangle. The Electronic Journal of Combinatorics, 12, R37.
Packing unit squares in a square $s(80)$	$\ge 9$	$\ge \sqrt{80}$	Lean proof	Nagamochi, H. (2005). Packing unit squares in a rectangle. The Electronic Journal of Combinatorics, 12, R37.
Packing unit squares in a square $s(82)$	$\ge {\approx}9.2667$	$\ge \sqrt{82}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(82)$	$\le 6+\frac{5}{\sqrt{2}}$	$\le 10$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(83)$	$\ge {\approx}9.2667$	$\ge \sqrt{83}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(83)$	$\le {\approx}9.6348$	$\le 10$	Lean proof	Allen Chang in September 2026
Packing unit squares in a square $s(84)$	$\ge {\approx}9.2667$	$\ge \sqrt{84}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(84)$	$\le 9+\frac{1}{\sqrt{2}}$	$\le 10$	Lean proof	F. Göbel, Geometrical Packing and Covering Problems, in Packing and Covering in Combinatorics, A. Schrijver (ed.), Math Centrum Tracts 106 (1979) 179-199.
Packing unit squares in a square $s(85)$	$\ge {\approx}9.2667$	$\ge \sqrt{85}$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(85)$	$\le \frac{11}{2}+3\sqrt{2}$	$\le 10$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(86)$	$\le \frac{17+\sqrt{7}}{2}$	$\le 10$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(87)$	$\le {\approx}9.8388$	$\le 10$	Lean proof	Allen Chang in September 2026
Packing unit squares in a square $s(88)$	$\le {\approx}9.8882$	$\le 10$	Lean proof	David W. Cantrell and David Ellsworth in January 2025
Packing unit squares in a square $s(89)$	$\le 5+\frac{7}{\sqrt{2}}$	$\le 10$	Lean proof	Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14
Packing unit squares in a square $s(98)$	$\ge 10$	$\ge \sqrt{98}$	Lean proof	Nagamochi, H. (2005). Packing unit squares in a rectangle. The Electronic Journal of Combinatorics, 12, R37.
Packing unit squares in a square $s(99)$	$\ge 10$	$\ge \sqrt{99}$	Lean proof	Nagamochi, H. (2005). Packing unit squares in a rectangle. The Electronic Journal of Combinatorics, 12, R37.