{"id":"palomar/PALOMAR-2026-08-20-000005","url":"https://github.com/google-deepmind/formal-conjectures/tree/d2e3d71ef64e3c7a67b0ea942d0a49e454a853b4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-20-000005-v1.json","repo":"https://github.com/google-deepmind/formal-conjectures","tags":["math.NT","math.AG","msc:11D41","msc:12E05","number-theory","perfect-cuboid","lean-formalization"],"score":0,"title":"google-deepmind/formal-conjectures","trust":"high","domain":"math.NT","source":"palomar","authors":["The Formal Conjectures Authors","Moritz Firsching","Codrut Grosu","Reklle"],"reviews":0,"subject":"math.NT","summary":"Formal proof of the First Cuboid Conjecture, which states that for all positive coprime integers a, b with a ≠ b, a certain degree-8 polynomial P_{a,b}(t) over ℤ is irreducible. This conjecture was proposed by Shapirov in \"Perfect cuboids and irreducible polynomials\" (arXiv:1108.5348) as part of a family of three conjectures whose combined truth would imply the nonexistence of a perfect Euler brick. The proof first analyses rational factors and the symmetry F(−x) vs F(x) to reduce irreducibility of the degree-8 polynomial to irreducibility of a degree-4 factor Q_{a,b}, and the coprime branch…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-20","reactions":{},"formalized":true}