{"id":"palomar/PALOMAR-2026-08-27-000019","url":"https://github.com/yuhangshi888/sun-cotangent-permanent-counterexample-lean/tree/8db902a56070f0d90866bf8a44d485a20cb817af","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000019-v1.json","repo":"https://github.com/yuhangshi888/sun-cotangent-permanent-counterexample-lean","tags":["math.NT","math.CO","msc:11C20","msc:15A15","msc:11A07","number-theory","lean","permanents","cotangent-sums"],"score":0,"title":"yuhangshi888/sun-cotangent-permanent-counterexample-lean","trust":"high","domain":"math.NT","source":"palomar","authors":["Yuhang Shi"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 and Mathlib formalization of the exact evaluation of the normalized 14 by 14 cotangent permanent at p = 29. The formalization proves that its value is 84643985981440 and hence gives a counterexample to the cotangent sign inequality in Zhi-Wei Sun's Conjecture 4.7(ii). It includes the analytic-to-cyclotomic bridge, two separately kernel-checked finite permanent certificates, Chinese-remainder and coefficientwise integer lifting, the Section 3 Archimedean uniqueness argument, and equation (4.1) in the integral cyclotomic quotient.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"A counterexample to Sun's sign conjecture for cotangent permanents","identifier":"doi:10.5281/zenodo.22105063","relationship":"formalizes"}]}