generate.py

back to table · edit · history · where entries came from · files · download

10040 bytes, as of the version from 2026-09-23 06:26 (current). Recorded here, not run.

"""Van der Waerden numbers w(r; k_1,...,k_r) -- numberdb.org/T440

This generator fills the draft table with the exact Van der Waerden numbers
listed in Wikipedia's known-values table. Entry comments cite the reference
named by the corresponding source row.

Run it with SageMath:

    $ sage -pip install numberdb          # once
    $ sage -python generate.py            # check the table against this code
    $ sage -python generate.py --publish  # fill the draft, with NUMBERDB_API_KEY set
"""

import os
import sys

import numberdb.sage as numberdb
from sage.rings.integer_ring import ZZ


TABLE = os.environ.get("NUMBERDB_TABLE", "T440")

SOURCE_COMMENTS = {
    'Ahmed2009': 'This value is due to Ahmed CITE{Ahmed2009}.',
    'Ahmed2010': 'This value is due to Ahmed CITE{Ahmed2010}.',
    'Ahmed2012': 'This value is due to Ahmed CITE{Ahmed2012}.',
    'Ahmed2013': 'This value is due to Ahmed CITE{Ahmed2013}.',
    'AhmedKullmannSnevily': 'This value is due to Ahmed, Kullmann and Snevily CITE{AhmedKullmannSnevily}.',
    'AhmedKullmannSnevily+Kouril2015': 'Ahmed, Kullmann and Snevily conjectured this value CITE{AhmedKullmannSnevily}; Kouril verified it CITE{Kouril2015}.',
    'Beeler': 'This value is due to Beeler CITE{Beeler}.',
    'BeelerONeil': "This value is due to Beeler and O'Neil CITE{BeelerONeil}.",
    'Brown': 'This value is due to Brown CITE{Brown}.',
    'Chvatal': 'This value is due to Chvátal CITE{Chvatal}.',
    'Karki': 'This value is due to Karki CITE{Karki}.',
    'Kouril2006': 'This value is due to Kouril CITE{Kouril2006}.',
    'Kouril2012': 'This value is due to Kouril CITE{Kouril2012}.',
    'Kouril2015': 'This value is due to Kouril CITE{Kouril2015}.',
    'KourilPaul': 'This value is due to Kouril and Paul CITE{KourilPaul}.',
    'LandmanRobertsonCulver': 'This value is due to Landman, Robertson and Culver CITE{LandmanRobertsonCulver}.',
    'Schweitzer': 'This value is due to Schweitzer CITE{Schweitzer}.',
    'StevensShantaram': 'This value is due to Stevens and Shantaram CITE{StevensShantaram}.',
}

SOURCE_ROWS = (
    (2, (3, 3), 9, 'Chvatal'),
    (2, (3, 4), 18, 'Chvatal'),
    (2, (3, 5), 22, 'Chvatal'),
    (2, (3, 6), 32, 'Chvatal'),
    (2, (3, 7), 46, 'Chvatal'),
    (2, (3, 8), 58, 'BeelerONeil'),
    (2, (3, 9), 77, 'BeelerONeil'),
    (2, (3, 10), 97, 'BeelerONeil'),
    (2, (3, 11), 114, 'LandmanRobertsonCulver'),
    (2, (3, 12), 135, 'LandmanRobertsonCulver'),
    (2, (3, 13), 160, 'LandmanRobertsonCulver'),
    (2, (3, 14), 186, 'Kouril2006'),
    (2, (3, 15), 218, 'Kouril2006'),
    (2, (3, 16), 238, 'Kouril2006'),
    (2, (3, 17), 279, 'Ahmed2010'),
    (2, (3, 18), 312, 'Ahmed2010'),
    (2, (3, 19), 349, 'AhmedKullmannSnevily'),
    (2, (3, 20), 389, 'AhmedKullmannSnevily+Kouril2015'),
    (2, (4, 4), 35, 'Chvatal'),
    (2, (4, 5), 55, 'Chvatal'),
    (2, (4, 6), 73, 'BeelerONeil'),
    (2, (4, 7), 109, 'Beeler'),
    (2, (4, 8), 146, 'Kouril2006'),
    (2, (4, 9), 309, 'Ahmed2012'),
    (2, (5, 5), 178, 'StevensShantaram'),
    (2, (5, 6), 206, 'Kouril2006'),
    (2, (5, 7), 260, 'Ahmed2013'),
    (2, (6, 6), 1132, 'KourilPaul'),
    (3, (2, 3, 3), 14, 'Brown'),
    (3, (2, 3, 4), 21, 'Brown'),
    (3, (2, 3, 5), 32, 'Brown'),
    (3, (2, 3, 6), 40, 'Brown'),
    (3, (2, 3, 7), 55, 'LandmanRobertsonCulver'),
    (3, (2, 3, 8), 72, 'Kouril2006'),
    (3, (2, 3, 9), 90, 'Ahmed2009'),
    (3, (2, 3, 10), 108, 'Ahmed2009'),
    (3, (2, 3, 11), 129, 'Ahmed2009'),
    (3, (2, 3, 12), 150, 'Ahmed2009'),
    (3, (2, 3, 13), 171, 'Ahmed2009'),
    (3, (2, 3, 14), 202, 'Kouril2012'),
    (3, (2, 4, 4), 40, 'Brown'),
    (3, (2, 4, 5), 71, 'Brown'),
    (3, (2, 4, 6), 83, 'LandmanRobertsonCulver'),
    (3, (2, 4, 7), 119, 'Kouril2006'),
    (3, (2, 4, 8), 157, 'Kouril2012'),
    (3, (2, 5, 5), 180, 'Ahmed2009'),
    (3, (2, 5, 6), 246, 'Kouril2012'),
    (3, (3, 3, 3), 27, 'Chvatal'),
    (3, (3, 3, 4), 51, 'BeelerONeil'),
    (3, (3, 3, 5), 80, 'LandmanRobertsonCulver'),
    (3, (3, 3, 6), 107, 'Ahmed2012'),
    (3, (3, 4, 4), 89, 'LandmanRobertsonCulver'),
    (3, (4, 4, 4), 293, 'Kouril2012'),
    (4, (2, 2, 3, 3), 17, 'Brown'),
    (4, (2, 2, 3, 4), 25, 'Brown'),
    (4, (2, 2, 3, 5), 43, 'Brown'),
    (4, (2, 2, 3, 6), 48, 'LandmanRobertsonCulver'),
    (4, (2, 2, 3, 7), 65, 'LandmanRobertsonCulver'),
    (4, (2, 2, 3, 8), 83, 'Ahmed2009'),
    (4, (2, 2, 3, 9), 99, 'Ahmed2009'),
    (4, (2, 2, 3, 10), 119, 'Ahmed2009'),
    (4, (2, 2, 3, 11), 141, 'Schweitzer'),
    (4, (2, 2, 3, 12), 163, 'Kouril2015'),
    (4, (2, 2, 4, 4), 53, 'Brown'),
    (4, (2, 2, 4, 5), 75, 'Ahmed2009'),
    (4, (2, 2, 4, 6), 93, 'Ahmed2009'),
    (4, (2, 2, 4, 7), 143, 'Kouril2012'),
    (4, (2, 3, 3, 3), 40, 'Brown'),
    (4, (2, 3, 3, 4), 60, 'LandmanRobertsonCulver'),
    (4, (2, 3, 3, 5), 86, 'Ahmed2009'),
    (4, (2, 3, 3, 6), 115, 'Kouril2015'),
    (4, (3, 3, 3, 3), 76, 'BeelerONeil'),
    (5, (2, 2, 2, 3, 3), 20, 'LandmanRobertsonCulver'),
    (5, (2, 2, 2, 3, 4), 29, 'Ahmed2009'),
    (5, (2, 2, 2, 3, 5), 44, 'Ahmed2009'),
    (5, (2, 2, 2, 3, 6), 56, 'Ahmed2009'),
    (5, (2, 2, 2, 3, 7), 72, 'Ahmed2009'),
    (5, (2, 2, 2, 3, 8), 88, 'Ahmed2009'),
    (5, (2, 2, 2, 3, 9), 107, 'Kouril2012'),
    (5, (2, 2, 2, 4, 4), 54, 'Ahmed2009'),
    (5, (2, 2, 2, 4, 5), 79, 'Ahmed2009'),
    (5, (2, 2, 2, 4, 6), 101, 'Kouril2012'),
    (5, (2, 2, 3, 3, 3), 41, 'LandmanRobertsonCulver'),
    (5, (2, 2, 3, 3, 4), 63, 'Ahmed2009'),
    (5, (2, 2, 3, 3, 5), 95, 'Kouril2015'),
    (6, (2, 2, 2, 2, 3, 3), 21, 'Ahmed2009'),
    (6, (2, 2, 2, 2, 3, 4), 33, 'Ahmed2009'),
    (6, (2, 2, 2, 2, 3, 5), 50, 'Ahmed2009'),
    (6, (2, 2, 2, 2, 3, 6), 60, 'Ahmed2009'),
    (6, (2, 2, 2, 2, 4, 4), 56, 'Ahmed2009'),
    (6, (2, 2, 2, 3, 3, 3), 42, 'Ahmed2009'),
    (7, (2, 2, 2, 2, 2, 3, 3), 24, 'Ahmed2009'),
    (7, (2, 2, 2, 2, 2, 3, 4), 36, 'Ahmed2009'),
    (7, (2, 2, 2, 2, 2, 3, 5), 55, 'Ahmed2012'),
    (7, (2, 2, 2, 2, 2, 3, 6), 65, 'Ahmed2013'),
    (7, (2, 2, 2, 2, 2, 4, 4), 66, 'Ahmed2013'),
    (7, (2, 2, 2, 2, 3, 3, 3), 45, 'Ahmed2013'),
    (8, (2, 2, 2, 2, 2, 2, 3, 3), 25, 'Ahmed2009'),
    (8, (2, 2, 2, 2, 2, 2, 3, 4), 40, 'Ahmed2012'),
    (8, (2, 2, 2, 2, 2, 2, 3, 5), 61, 'Ahmed2013'),
    (8, (2, 2, 2, 2, 2, 2, 3, 6), 71, 'Ahmed2013'),
    (8, (2, 2, 2, 2, 2, 2, 4, 4), 67, 'Ahmed2013'),
    (8, (2, 2, 2, 2, 2, 3, 3, 3), 49, 'Ahmed2013'),
    (9, (2, 2, 2, 2, 2, 2, 2, 3, 3), 28, 'Ahmed2009'),
    (9, (2, 2, 2, 2, 2, 2, 2, 3, 4), 42, 'Ahmed2013'),
    (9, (2, 2, 2, 2, 2, 2, 2, 3, 5), 65, 'Ahmed2013'),
    (9, (2, 2, 2, 2, 2, 2, 3, 3, 3), 52, 'Ahmed2013'),
    (10, (2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 31, 'Ahmed2013'),
    (10, (2, 2, 2, 2, 2, 2, 2, 2, 3, 4), 45, 'Ahmed2013'),
    (10, (2, 2, 2, 2, 2, 2, 2, 2, 3, 5), 70, 'Ahmed2013'),
    (11, (2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 33, 'Ahmed2013'),
    (11, (2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 4), 48, 'Ahmed2013'),
    (12, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 35, 'Ahmed2013'),
    (12, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 4), 52, 'Ahmed2013'),
    (13, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 37, 'Ahmed2013'),
    (13, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 4), 55, 'Ahmed2013'),
    (14, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 39, 'Ahmed2013'),
    (15, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 42, 'Ahmed2013'),
    (16, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 44, 'Ahmed2013'),
    (17, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 46, 'Ahmed2013'),
    (18, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 48, 'Ahmed2013'),
    (19, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 50, 'Ahmed2013'),
    (20, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 51, 'Ahmed2013'),
    (21, (2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3), 52, 'Karki'),
)


def _key_from_stdin():
    if os.environ.get("NUMBERDB_KEY_FROM_STDIN") != "1":
        return
    token = sys.stdin.read().strip()
    if "=" in token and token.split("=", 1)[0].isupper():
        token = token.split("=", 1)[1].strip().strip("'\"")
    if token:
        os.environ["NUMBERDB_API_KEY"] = token


def _tuple_text(parts):
    return ",".join(str(part) for part in parts)


def _check_parameters(r, parts):
    if r != len(parts):
        raise ValueError("r=%s but k has %s parts" % (r, len(parts)))
    if tuple(sorted(parts)) != parts:
        raise ValueError("k is not weakly increasing: %r" % (parts,))
    if any(part < 1 for part in parts):
        raise ValueError("all progression lengths must be positive: %r" % (parts,))


def _all_rows():
    rows = {}
    for r, parts, value, source in SOURCE_ROWS:
        _check_parameters(r, parts)
        if r == 1 or all(part == 2 for part in parts):
            raise AssertionError("trivial formula row is not part of the source table")
        if source not in SOURCE_COMMENTS:
            raise AssertionError("no source comment for %s" % (source,))
        rows[(r, parts)] = (value, source)
    if len(SOURCE_ROWS) != 124:
        raise AssertionError("the transcribed source table should have 124 rows")
    return rows


VALUES = _all_rows()


class VanDerWaerdenNumbers(numberdb.Generator):

    table = TABLE
    parameters = ("r", "k")
    type = "Z"
    rigour = "exact"

    def enumerate(self):
        for r, parts in sorted(VALUES):
            yield {"r": str(r), "k": _tuple_text(parts)}

    def value(self, params, digits):
        r = int(params["r"])
        parts = tuple(int(part) for part in params["k"].split(","))
        _check_parameters(r, parts)
        number, source = VALUES[(r, parts)]
        return {"number": ZZ(number), "comment": SOURCE_COMMENTS[source]}


if __name__ == "__main__":
    _key_from_stdin()
    generator = VanDerWaerdenNumbers()
    if os.environ.get("NUMBERDB_PUBLISH") == "1" or "--publish" in sys.argv:
        print(generator.publish(message="fill exact van der Waerden numbers"))
    else:
        report = generator.verify(sample=None)
        print(report)
        sys.exit(0 if report.ok else 1)