{"id":"palomar/PALOMAR-2026-09-11-000004","url":"https://github.com/BrandonMYates/allones-comparator/tree/76f3a65407c45de21228824f7a41430acec473a4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-11-000004-v1.json","repo":"https://github.com/BrandonMYates/allones-comparator","tags":["math.NT","msc:11T06","msc:12E20","finite-fields","lean","polynomials"],"score":0,"title":"All-ones polynomials over GF(2) under the substitution X ↦ X² + X + 1 (OEIS A071642, TheoremDB P12771)","trust":"high","domain":"math.NT","source":"palomar","authors":["Brandon Yates"],"reviews":0,"subject":"math.NT","summary":"Formalizes in Lean 4 the resolution of a 2019 OEIS conjecture of L. H. Gallardo (comment on A071642; TheoremDB P12771): for every n ≥ 2 the all-ones polynomial 1 + X + ⋯ + Xⁿ is irreducible over GF(2) if and only if 1 + P + ⋯ + Pⁿ is irreducible over GF(2), where P = X² + X + 1. The compared statements are the per-n equivalence, the literal set-level form of the OEIS comment (the terms ≥ 2 coincide), and the failure of the excluded case n = 1. The proof is elementary: a factorization of the all-ones polynomial composes to one of the substituted polynomial; conversely irreducibility forces n…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-11","reactions":{},"formalized":true}