arXiv·arxiv:2607.05739/TanArctanSum

Integer values of tan(arctan 1 + arctan 2 + ⋯ + arctan n)

conjecture formal record: mixed F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

Fidelity F2: The correspondence is declared through a Comparator challenge and an alignment table.

AI activity

No AI contribution recorded against this statement.

F2 declared. The correspondence is declared through a Comparator challenge and an alignment table.

As each project's formalization.yaml states it.

TanArctanAxiomMath/TanArctan · joined by artifact · no independent check

authors: Kenny Lau
method: autonomous — AxiomProver
review: author-verified (Kenny Lau)
axioms: Classical.choice, Quot.sound, propext
sorry: 0 unproved goals declared
results: 3 main results named, checked with Comparator, with an alignment table
sources: Integer values of $\tan(\arctan 1+\arctan 2+\cdots+\arctan n)$ are rare — formalizes
checked by: nobody independent of its authors yet

Follow this problem

An email when it has a new claim, check, bounty or discussion. You confirm once and can stop with one click.

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal statements · 1

FormalConjectures/Arxiv/2607.05739/TanArctanSum.lean
9 declarations, 7 unproved goals·research open, research solved, test, textbook

Cited proofs · 3

Also known as · 2

https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Arxiv/2607.05739/TanArctanSum.lean
FormalConjectures/Arxiv/2607.05739/TanArctanSum.lean

qed.bot, “Integer values of tan(arctan 1 + arctan 2 + ⋯ + arctan n)”, https://qed.bot/s/arxiv-2607-05739-tanarctansum, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.