Open Research Index

yuhangshi888/sun-cotangent-permanent-counterexample-lean

Yuhang Shi

Palomar Registrypalomar/PALOMAR-2026-08-27-000019Aug 27, 2026math.NTscore 0

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-27-000019
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000019/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000019/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'