ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Machin's formula $π / 4 = 4 \arctan (1 / 5) - \arctan (1 / 239)$

Example

Machin's formula is

$\frac{π}{4} = 4 \arctan \frac{1}{5} - \arctan \frac{1}{239} .$

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Principal arctangent takes values in $(- π / 2, π / 2)$ , is the inverse of tangent there, and is strictly increasing (The principal inverse tangent $\arctan : R \to (- π / 2, π / 2)$ , Tangent is a continuous strictly increasing bijection from $(- π / 2, π / 2)$ onto $R$ ).

[L2]

The tangent addition and subtraction formulas hold when their displayed denominators and domains are nonzero (Addition and subtraction formulas for tangent, cotangent, secant, and cosecant on their exact domains).

[L3]

Tangent is the quotient of sine by cosine; $\sin 0 = 0$ and $\cos 0 = 1$ ; and the cofunction and Pythagorean identities give $\tan (π / 4) = 1$ (Tangent, cotangent, secant, and cosecant on their exact natural domains, The derivatives of sine and cosine are cosine and minus sine, Cofunction, supplementary, quarter-turn, and reflection identities for the six trigonometric functions, Pythagorean and parity identities for all six trigonometric functions on their natural domains).

Proof

technique · direct

1.1

Put $a : = \arctan (1 / 5)$ and $b : = \arctan (1 / 239)$ . Then $\tan a = 1 / 5$ and $\tan b = 1 / 239$ . Comparing with $\tan 0 = 0$ and [L3] on the principal branch gives $0 < a, b < π / 4$ .

L1L3

2.1

Since $0 < a < π / 4$ , we have $0 < 2 a < π / 2$ , so the tangent addition formula applies. It gives $\tan (2 a) = \frac{5}{12} < 1 = \tan (π / 4) .$ Strict increase of tangent on the principal branch now gives $2 a < π / 4$ , hence $0 < 4 a < π / 2$ .

step 1.1L1L2L3algebra

3.1

The addition formula, now applied to $2 a + 2 a$ , gives $\tan (4 a) = \frac{120}{119} > 1.$ All displayed denominators are positive.

step 2.1L2algebra

4.1

A final use of [L2] gives $\tan (4 a - b) = \frac{120 / 119 - 1 / 239}{1 + (120 / 119) (1 / 239)} = 1.$ The denominator is positive.

step 1.1step 3.1L2algebra

4.2

By step 2.1, $4 a$ lies in the principal tangent interval. Since $\tan (4 a) > 1 = \tan (π / 4)$ , strict increase gives $4 a > π / 4 > b$ . Thus $0 < 4 a - b < 4 a < π / 2$ . Consequently $4 a - b$ and $π / 4$ lie in the same injective branch of tangent.

step 1.1step 2.1step 3.1L1L3

5.1

Steps 4.1 and 4.2 imply $4 a - b = π / 4$ , which is the claimed formula.

step 4.1step 4.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

NIST Digital Library of Mathematical Functions, §4.24(iii) Addition Formulas (standard reference, not scraped)

Machin's formula π/4=4arctan⁡(1/5)−arctan⁡(1/239)π/4=4arctan(1/5)−arctan(1/239)