ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 $\pi/4=4\arctan(1/5)-\arctan(1/239)$

Example

Machin's formula is

$\frac\pi4=4\arctan\frac15-\arctan\frac1{239}.$

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Principal arctangent takes values in $(-\pi/2,\pi/2)$ , is the inverse of tangent there, and is strictly increasing (The principal inverse tangent $\arctan:\mathbb R\to(-\pi/2,\pi/2)$ , Tangent is a continuous strictly increasing bijection from $(-\pi/2,\pi/2)$ onto $\mathbb 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; $\sin0=0$ and $\cos0=1$ ; and the cofunction and Pythagorean identities give $\tan(\pi/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 $\tan0=0$ and [L3] on the principal branch gives $0<a,b<\pi/4$ .

L1L3

2.1

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

step 1.1L1L2L3algebra

3.1

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

step 2.1L2algebra

4.1

A final use of [L2] gives $\tan(4a-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, $4a$ lies in the principal tangent interval. Since $\tan(4a)>1=\tan(\pi/4)$ , strict increase gives $4a>\pi/4>b$ . Thus $0<4a-b<4a<\pi/2$ . Consequently $4a-b$ and $\pi/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 $4a-b=\pi/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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 65 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)\pi/4=4\arctan(1/5)-\arctan(1/239)π/4=4arctan(1/5)−arctan(1/239)