Revision #3488 → #4034 · back to history
modifiedPons asinorum (Book I, Prop. 5)76ecea39726d
| Field | From #3488 | To #4034 |
|---|
| note | Verified: EuclideanGeometry.angle_eq_angle_of_dist_eq states dist p₁ p₂ = dist p₁ p₃ → angle p₁ p₂ p₃ = angle p₁ p₃ p₂, the pons asinorum. | Verified via decl_exists: EuclideanGeometry.angle_eq_angle_of_dist_eq gives dist p₁ p₂ = dist p₁ p₃ → angle p₁ p₂ p₃ = angle p₁ p₃ p₂, the pons asinorum. |
modifiedPythagorean theorem (Book I, Props. 47–48)764d4483eb8f
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Mathlib formalizes the Pythagorean theorem in inner-product/Euclidean form as an iff with the right-angle condition. | Verified via decl_exists: Mathlib formalizes the Pythagorean theorem in inner-product form as an iff with the right-angle condition. |
modifiedGolden ratio / extreme and mean ratio (Book II, Prop. 11)c9c467bfca19
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Real.goldenRatio := (1 + √5)/2 with its irrationality and algebraic identities. | Verified via decl_exists: Real.goldenRatio := (1 + √5)/2 lives in Mathlib.NumberTheory.Real.GoldenRatio. |
modifiedInscribed angle theorem (Book III, Prop. 20)98264284fa51
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Mathlib states the central-angle = 2·inscribed-angle relation for oriented angles on a circle. | Verified via decl_exists: Mathlib states the central-angle = 2·inscribed-angle relation for oriented angles on a circle. |
modifiedThales's theorem (Book III, Prop. 31)8b83f731271b
| Field | From #3488 | To #4034 |
|---|
| note | Verified: angle p₁ p₂ p₃ = π/2 iff p₂ lies on the sphere with diameter p₁p₃. | Verified via decl_exists: angle p₁ p₂ p₃ = π/2 iff p₂ lies on the sphere with diameter p₁p₃. |
modifiedIntersecting chords theorem (Book III, Prop. 35)2bef93b09634
| Field | From #3488 | To #4034 |
|---|
| note | Verified: intersecting chords theorem stated via cospherical points and the power-of-a-point file. | Verified via decl_exists: intersecting chords theorem stated via cospherical points in Sphere/Power. |
modifiedTangent–secant theorem (Book III, Prop. 36)2b836fe27320
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Sphere.Power file proves the tangent–secant theorem. | Verified via decl_exists: Sphere.Power file proves the tangent–secant theorem. |
modifiedEuclid's theorem on infinitude of primes (Book IX, Prop. 20)b07c197005df
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Nat.exists_infinite_primes gives ∀ n, ∃ p ≥ n, p prime — Euclid's theorem. | Verified via decl_exists: Nat.exists_infinite_primes gives ∀ n, ∃ p ≥ n, p prime — Euclid's theorem. |
modifiedSum of a finite geometric series (Book IX, Prop. 35)747957e93ad3
| Field | From #3488 | To #4034 |
|---|
| note | Verified: geom_sum_eq gives ∑ xⁱ = (xⁿ − 1)/(x − 1) in a field, the standard finite geometric-series formula. | Verified via decl_exists: geom_sum_eq gives ∑ xⁱ = (xⁿ − 1)/(x − 1) in a field, the standard finite geometric-series formula. |
modifiedConstruction of even perfect numbers (Book IX, Prop. 36)928720baa2b2
| Field | From #3488 | To #4034 |
|---|
| mathlib.decl | — | Theorems100.Nat.perfect_two_pow_mul_mersenne_of_prime |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Archive.Wiedijk100Theorems.PerfectNumbers |
| note | Semantic search confirms Mathlib has Nat.Perfect and mersenne but no theorem that 2^(p−1)·(2^p−1) is perfect when 2^p−1 is prime. | Verified via decl_exists: the Wiedijk-100 archive proves Euclid IX.36 — if mersenne (k+1) is prime then 2^k · mersenne (k+1) is perfect; the previously cited Nat.Perfect.two_pow_mul_mersenne_of_prime does not exist. |
| status | not_formalized | formalized |
modifiedPerfect number755fc640e82f
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Nat.Perfect n is defined as the proper-divisor sum equalling n with n positive. | Verified via decl_exists: Nat.Perfect n is defined as the proper-divisor sum equalling n with n positive. |
modifiedEuclid–Euler theoremd34bb58db9d4
| Field | From #3488 | To #4034 |
|---|
| mathlib.decl | — | Theorems100.Nat.even_and_perfect_iff |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Archive.Wiedijk100Theorems.PerfectNumbers |
| note | Semantic search shows no Mathlib decl characterizes even perfect numbers via Mersenne primes. | Verified via decl_exists: the Wiedijk-100 archive proves Euclid–Euler as even_and_perfect_iff characterizing even perfect numbers; the previously cited Theorems100.Perfect.iff_mersenne_prime does not exist. |
| status | not_formalized | formalized |
modifiedIrrationality of square roots of non-square integers (Book X, Prop. 9)03e5064b8c57
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Irrational (√z) ↔ ¬IsSquare z for nonneg integers — Book X Prop 9. | Verified via decl_exists: Irrational (√z) ↔ ¬IsSquare z for nonneg integers — Book X Prop 9. |
modifiedEuclid's formula for Pythagorean triples (Book X, lemma to Prop. 29)c10f1d4e7b78
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Mathlib classifies primitive Pythagorean triples in the (m²−n², 2mn, m²+n²) Euclidean form. | Verified via decl_exists: Mathlib classifies primitive Pythagorean triples in the (m²−n², 2mn, m²+n²) Euclidean form. |
modifiedVolume of sphere proportional to cube of radius (Book XII)3500a2760720
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Mathlib computes vol(ball) = r³ · (4π/3) in ℝ³, exhibiting the r³ proportionality. | Verified via decl_exists: Mathlib computes vol(ball) = r³ · (4π/3) in ℝ³, exhibiting the r³ proportionality. |
modifiedEuclidean algorithm for GCD (Book VII, Props. 1–4)aebc0ce23db9
| Field | From #3488 | To #4034 |
|---|
| mathlib.module | Mathlib.Data.Nat.GCD.Basic | Init.Data.Nat.Gcd |
| note | Verified: Nat.gcd is defined by the Euclidean recursion gcd a b = gcd (b % a) a and its correctness lemmas (Nat.gcd_dvd_left, Nat.dvd_gcd) live in Mathlib's GCD/Basic. | Verified via decl_exists: Nat.gcd (Lean core, re-exported through Mathlib) is defined by the Euclidean recursion gcd a b = gcd (b % a) a; its correctness API lives in Mathlib.Data.Nat.GCD.Basic. |
modifiedLaw of cosines (geometric precursor in Book II)363a54672206
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Mathlib formalizes the law of cosines in inner-product form, generalizing Book II Props 12–13. | Verified via decl_exists: Mathlib formalizes the law of cosines in inner-product form, generalizing Book II Props 12–13. |
modifiedIrrationality of √2 (Book X)1232c5b7ff73
| Field | From #3488 | To #4034 |
|---|
| note | Verified: Nat.Prime.irrational_sqrt yields irrationality of √p for every prime p, in particular √2. | Verified via decl_exists: Nat.Prime.irrational_sqrt yields irrationality of √p for every prime p, in particular √2. |
modifiedThales' theorem (mention in lead)9141c22c1e6c
| Field | From #3488 | To #4034 |
|---|
| note | Verified: same decl as Book III Prop. 31; Thales' theorem is that an angle inscribed in a semicircle is a right angle. | Verified via decl_exists: same decl as Book III Prop. 31; Thales' theorem is that an angle inscribed in a semicircle is a right angle. |
addedPrime number (Book VII definitions)3566b23e7f1f
addedLeast common multiple (Book VII, Props. 33–39)062386b54680
addedEven and odd numbers (Book VII, parity definitions)7b561e69acc2