Lean repository linked
Integer values of tan(arctan 1+arctan 2+⋯+arctan n) are rare
arXiv:2607.05739 · arXiv
Lean formalisations (1)
AxiomMath/TanArctan at 344aa3213959
Linked by the repository’s formalization.yaml.
Project review: author-verified
Audit: awaiting publication.