Claims

../

1991_12_01_furstenberg_katznelson: Furstenberg and Katznelson's 1991 density Hales-Jewett theorem, whose three-letter case gives that a subset of the ternary n-cube with no three collinear points has size o(3^n); refereed, credited by the site.

2012_09_22_dodos_kanellopoulos_tyros: Dodos, Kanellopoulos and Tyros's 2012 combinatorial proof of the density Hales-Jewett theorem, whose ternary case gives f_3(n)=o(3^n) since a combinatorial line is collinear; refereed; a Lean formalization exists, not built here.

---