Integer values of \tan(\arctan 1+\arctan 2+\cdots+\arctan n) are rare
AI use, as the source states it
“The results in this note were formalized in Lean/Mathlib and produced autonomously by AxiomProver from natural-language statements.”
Model: AxiomProver, as stated
Named here, or see a mistake? Write to privacy@papex.org.