Humanities Helping Hands
Every Proven Fact
The 167 facts on the Proven Atlas as one plain list, from the floor of proven math up to the observable universe. 118 were checked by Lean, 49 by the browser checker (the numbers only, not the real-world part).
The floor: proven math (102)
- Daniel's Root Theorem: fixing a mistake once, at the root, never costs more than fixing its copies in every layer above it, and costs strictly less once it has spread to two or more layers
c ≤ n × c, and c < n × c when n ≥ 2 and c > 0 Checked by Lean, theorem DanielRootTheorem. See it on the map - Daniel's Founder's Claim: if, every week, the library of proven facts grows at least as much as the cost of finding a new one, its lead never shrinks; if it grows strictly more, the lead grows every week
facts − cost never falls when Δfacts ≥ Δcost each week, and strictly rises when Δfacts > Δcost Checked by Lean, theorem DanielFounderClaim. See it on the map - P vs NP, the easy half: checking a proposed answer to any SAT puzzle (Boolean rules over switches) is fast and right, so SAT is in NP
the checker says yes exactly when every rule is met, in at most one step per switch mention and per rule, plus one Checked by Lean, theorem PvsNP.sat_check_is_fast_and_right. See it on the map - one specified outcome in 1,000
1/1000 Checked by Lean, theorem TowerBatch.p21_rare_one_in_1000. See it on the map - Area under a curve: y = x^2 from 0 to 3
9 Checked by Lean, theorem CalculusLane.p30_area_under_square. See it on the map - Markov token: reaching the win square before the lose square
4/7 Checked by Lean, theorem CheapLane.p32_markov_token_absorption_limit. See it on the map - Random walk: reaching +3 within 12 steps
397/1024 Checked by Lean, theorem p37_random_walk_hits_three. See it on the map - Two-dimensional walk: back at the start after 6 steps
25/256 Checked by Lean, theorem CheapLane.p38_random_walk_2d. See it on the map - Random walk: expected highest point in 10 steps
251/128 Checked by Lean, theorem CheapLane.p39_expected_max. See it on the map - At least 3 successes in 12 trials, each a success with chance 1/3
435185/531441 Checked by Lean, theorem TowerBatch.p48_third_success_by_twelve. See it on the map - Random walk: never below the start and back at it after 12 steps
33/1024 Checked by Lean, theorem p52_random_walk_never_negative. See it on the map - two numbers up to 1,000 share no common factor
608383/1000000 Checked by Lean, theorem CheapLane.p63_trap_coprime_pair_finite. See it on the map - Integral: area under exp(x) from 0 to 1
e-1 Checked by Lean, theorem CalculusLane.p91_exp_area. See it on the map - Integral: area under one arch of the sine curve
2 Checked by Lean, theorem CalculusLane.p92_sine_arch. See it on the map - Series: the sum of 1/k^2 over all positive integers
pi^2/6 Checked by Lean, theorem SeriesLane.p93_basel. See it on the map - Series: the sum of k/2^k over all positive integers
2 Checked by Lean, theorem SeriesLane.p94_k_over_two_pow. See it on the map - Root finding: the positive root of x^2 = 2
sqrt(2) Checked by Lean, theorem RootsLane.p95_positive_root_of_two. See it on the map - ODE: value of the oscillator y'' + 4y = 0 at t = pi/6
1/2 Checked by Lean, theorem CalculusLane.p98_oscillator. See it on the map - Series: the sum of 1/(k(k+1)) over all positive integers
1 Checked by Lean, theorem SeriesLane.p99_telescoping. See it on the map - Integral: area under log(x)/x from 1 to e
1/2 Checked by Lean, theorem CalculusLane.p100_log_over_x. See it on the map - There are infinitely many prime numbers: past any number, there is always another prime
Nat.exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p Checked by Lean (Mathlib), theorem Nat.exists_infinite_primes. See it on the map - Bertrand's postulate: between any whole number n above zero and 2n there is always a prime
Nat.exists_prime_lt_and_le_two_mul (n : ℕ) (hn0 : n ≠ 0) : ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n Checked by Lean (Mathlib), theorem Nat.exists_prime_lt_and_le_two_mul. See it on the map - Dirichlet's theorem: if a and n share no factor, infinitely many primes leave remainder a when divided by n
Nat.infinite_setOfPred_prime_and_eq_mod {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) : {p | Nat.Prime p ∧ ↑p = a}.Infinite Checked by Lean (Mathlib), theorem Nat.infinite_setOfPred_prime_and_eq_mod. See it on the map - The square root of 2 is not a fraction of two whole numbers
irrational_sqrt_two : Irrational √2 Checked by Lean (Mathlib), theorem irrational_sqrt_two. See it on the map - Pi is not a fraction of two whole numbers
irrational_pi : Irrational Real.pi Checked by Lean (Mathlib), theorem irrational_pi. See it on the map - The golden ratio is not a fraction of two whole numbers
Real.goldenRatio_irrational : Irrational Real.goldenRatio Checked by Lean (Mathlib), theorem Real.goldenRatio_irrational. See it on the map - Liouville numbers are transcendental: they are not the root of any polynomial with whole-number coefficients
Liouville.transcendental {x : ℝ} (lx : Liouville x) : Transcendental ℤ x Checked by Lean (Mathlib), theorem Liouville.transcendental. See it on the map - Pi is bigger than 3
Real.pi_gt_three : 3 < Real.pi Checked by Lean (Mathlib), theorem Real.pi_gt_three. See it on the map - Pi is bigger than 3.14
Real.pi_gt_d2 : 3.14 < Real.pi Checked by Lean (Mathlib), theorem Real.pi_gt_d2. See it on the map - Pi is smaller than 3.15
Real.pi_lt_d2 : Real.pi < 3.15 Checked by Lean (Mathlib), theorem Real.pi_lt_d2. See it on the map - Euler's identity: e raised to pi times i equals -1
Complex.exp_pi_mul_I : Complex.exp (↑Real.pi * Complex.I) = -1 Checked by Lean (Mathlib), theorem Complex.exp_pi_mul_I. See it on the map - For every angle, sine squared plus cosine squared equals 1
Real.sin_sq_add_cos_sq (x : ℝ) : Real.sin x ^ 2 + Real.cos x ^ 2 = 1 Checked by Lean (Mathlib), theorem Real.sin_sq_add_cos_sq. See it on the map - The Basel problem: 1 + 1/4 + 1/9 + 1/16 + ... adds up to exactly pi squared over 6
hasSum_zeta_two : HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6) Checked by Lean (Mathlib), theorem hasSum_zeta_two. See it on the map - The harmonic series 1 + 1/2 + 1/3 + 1/4 + ... grows past every number
Real.tendsto_sum_range_one_div_nat_succ_atTop : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, 1 / (↑i + 1)) Filter.atTop Filter.atTop Checked by Lean (Mathlib), theorem Real.tendsto_sum_range_one_div_nat_succ_atTop. See it on the map - Gauss's sum: twice the sum 0 + 1 + ... + (n - 1) equals n times (n - 1)
Finset.sum_range_id_mul_two (n : ℕ) : (∑ i ∈ Finset.range n, i) * 2 = n * (n - 1) Checked by Lean (Mathlib), theorem Finset.sum_range_id_mul_two. See it on the map - Adding up row n of Pascal's triangle gives exactly 2 to the power n
Nat.sum_range_choose (n : ℕ) : ∑ m ∈ Finset.range (n + 1), n.choose m = 2 ^ n Checked by Lean (Mathlib), theorem Nat.sum_range_choose. See it on the map - A set with n things has exactly 2 to the power n subsets
Finset.card_powerset.{u_1} {α : Type u_1} (s : Finset α) : s.powerset.card = 2 ^ s.card Checked by Lean (Mathlib), theorem Finset.card_powerset. See it on the map - n different things can be put in order in exactly n factorial ways
Fintype.card_perm.{u_1} {α : Type u_1} [DecidableEq α] [Fintype α] : Fintype.card (Equiv.Perm α) = (Fintype.card α).factorial Checked by Lean (Mathlib), theorem Fintype.card_perm. See it on the map - Fermat's little theorem: for a prime p, any number not divisible by p, raised to p - 1, leaves remainder 1 when divided by p
ZMod.pow_card_sub_one_eq_one {p : ℕ} [Fact (Nat.Prime p)] {a : ZMod p} (ha : a ≠ 0) : a ^ (p - 1) = 1 Checked by Lean (Mathlib), theorem ZMod.pow_card_sub_one_eq_one. See it on the map - Wilson's theorem: for a prime p, (p - 1) factorial leaves remainder p - 1 when divided by p
ZMod.wilsons_lemma (p : ℕ) [Fact (Nat.Prime p)] : ↑(p - 1).factorial = -1 Checked by Lean (Mathlib), theorem ZMod.wilsons_lemma. See it on the map - Fermat's two squares theorem: every prime that leaves remainder 1 when divided by 4 is a sum of two squares
Nat.Prime.sq_add_sq {p : ℕ} [Fact (Nat.Prime p)] (hp : p % 4 ≠ 3) : ∃ a b, a ^ 2 + b ^ 2 = p Checked by Lean (Mathlib), theorem Nat.Prime.sq_add_sq. See it on the map - Lagrange's four squares theorem: every whole number is a sum of four squares
Nat.sum_four_squares (n : ℕ) : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n Checked by Lean (Mathlib), theorem Nat.sum_four_squares. See it on the map - Quadratic reciprocity: for two different odd primes, whether each is a square remainder for the other is linked by one exact sign rule
legendreSym.quadratic_reciprocity {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) : legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2)) Checked by Lean (Mathlib), theorem legendreSym.quadratic_reciprocity. See it on the map - Fermat's Last Theorem for power 4: no whole numbers above zero solve a^4 + b^4 = c^4
fermatLastTheoremFour : FermatLastTheoremFor 4 Checked by Lean (Mathlib), theorem fermatLastTheoremFour. See it on the map - Fermat's Last Theorem for power 3: no whole numbers above zero solve a^3 + b^3 = c^3
fermatLastTheoremThree : FermatLastTheoremFor 3 Checked by Lean (Mathlib), theorem fermatLastTheoremThree. See it on the map - The fundamental theorem of algebra: every polynomial of degree 1 or more has a root among the complex numbers
Complex.exists_root {f : Polynomial ℂ} (hf : 0 < f.degree) : ∃ z, f.IsRoot z Checked by Lean (Mathlib), theorem Complex.exists_root. See it on the map - The intermediate value theorem: a continuous curve from a low point to a high point passes through every height in between
intermediate_value_Icc.{u, u_1} {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b Checked by Lean (Mathlib), theorem intermediate_value_Icc. See it on the map - The extreme value theorem: a continuous function on a closed, bounded, non-empty set reaches a lowest value
IsCompact.exists_isMinOn.{u_2, u_3} {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, IsMinOn f s x Checked by Lean (Mathlib), theorem IsCompact.exists_isMinOn. See it on the map - The mean value theorem: a smooth curve somewhere has a slope equal to the average slope between its two ends
exists_hasDerivAt_eq_slope (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) : ∃ c ∈ Set.Ioo a b, f' c = (f b - f a) / (b - a) Checked by Lean (Mathlib), theorem exists_hasDerivAt_eq_slope. See it on the map - Cantor's theorem: every set has strictly more subsets than it has members, even an infinite one
Cardinal.cantor.{u} (a : Cardinal.{u}) : a < 2 ^ a Checked by Lean (Mathlib), theorem Cardinal.cantor. See it on the map - The real numbers cannot be listed one by one: there are more of them than whole numbers
Cardinal.not_countable_real : ¬Set.univ.Countable Checked by Lean (Mathlib), theorem Cardinal.not_countable_real. See it on the map - Lagrange's theorem: in a finite group, the size of any subgroup divides the size of the group
Subgroup.card_subgroup_dvd_card.{u_1} {α : Type u_1} [Group α] (s : Subgroup α) : Nat.card ↥s ∣ Nat.card α Checked by Lean (Mathlib), theorem Subgroup.card_subgroup_dvd_card. See it on the map - Sylow's first theorem: if p^n divides the size of a finite group, the group has a subgroup of exactly that size
Sylow.exists_subgroup_card_pow_prime.{u} {G : Type u} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact (Nat.Prime p)] (hdvd : p ^ n ∣ Nat.card G) : ∃ K, Nat.card ↥K = p ^ n Checked by Lean (Mathlib), theorem Sylow.exists_subgroup_card_pow_prime. See it on the map - Pythagoras: in a triangle, the long side squared equals the sum of the other two squared exactly when their angle is a right angle
EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two.{u_1, u_2} {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 Checked by Lean (Mathlib), theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two. See it on the map - The Cauchy-Schwarz inequality: the size of the dot product of two real vectors is never bigger than their lengths multiplied
abs_real_inner_le_norm.{u_3} {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) : |inner ℝ x y| ≤ ‖x‖ * ‖y‖ Checked by Lean (Mathlib), theorem abs_real_inner_le_norm. See it on the map - The number e is bigger than 2.7182818283
Real.exp_one_gt_d9 : 2.7182818283 < Real.exp 1 Checked by Lean (Mathlib), theorem Real.exp_one_gt_d9. See it on the map - The number e is smaller than 2.7182818286
Real.exp_one_lt_d9 : Real.exp 1 < 2.7182818286 Checked by Lean (Mathlib), theorem Real.exp_one_lt_d9. See it on the map - Every prime number is at least 2
Nat.Prime.two_le {p : ℕ} : Nat.Prime p → 2 ≤ p Checked by Lean (Mathlib), theorem Nat.Prime.two_le. See it on the map - Euler's theorem: a number with no factor in common with n, raised to the count of such numbers below n, leaves remainder 1 when divided by n
Nat.ModEq.pow_totient {x n : ℕ} (h : x.Coprime n) : x ^ n.totient ≡ 1 [MOD n] Checked by Lean (Mathlib), theorem Nat.ModEq.pow_totient. See it on the map - For any two whole numbers, their greatest common divisor times their least common multiple equals the two numbers multiplied
Nat.gcd_mul_lcm (m n : ℕ) : m.gcd n * m.lcm n = m * n Checked by Lean (Mathlib), theorem Nat.gcd_mul_lcm. See it on the map - Bezout's identity: the greatest common divisor of two numbers is always a whole-number combination of them
Nat.gcd_eq_gcd_ab (x y : ℕ) : ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y Checked by Lean (Mathlib), theorem Nat.gcd_eq_gcd_ab. See it on the map - Every whole number other than 1 has a prime number that divides it
Nat.exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Nat.Prime p ∧ p ∣ n Checked by Lean (Mathlib), theorem Nat.exists_prime_and_dvd. See it on the map - The square root of any prime number is irrational: no fraction equals it
Nat.Prime.irrational_sqrt {p : ℕ} (hp : Nat.Prime p) : Irrational √↑p Checked by Lean (Mathlib), theorem Nat.Prime.irrational_sqrt. See it on the map - The binomial theorem: (x + y) to the power n expands into a sum with the binomial coefficients
add_pow.{u_1} {R : Type u_1} [CommSemiring R] (x y : R) (n : ℕ) : (x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m) Checked by Lean (Mathlib), theorem add_pow. See it on the map - The pigeonhole principle: put more things into fewer boxes and some box gets two
Finset.exists_ne_map_eq_of_card_lt_of_maps_to.{u_1, u_2} {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (hc : t.card < s.card) {f : α → β} (hf : Set.MapsTo f ↑s ↑t) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y Checked by Lean (Mathlib), theorem Finset.exists_ne_map_eq_of_card_lt_of_maps_to. See it on the map - A geometric series 1 + r + r^2 + ... with r between 0 and 1 adds up to exactly 1 / (1 - r)
tsum_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : ∑' (n : ℕ), r ^ n = (1 - r)⁻¹ Checked by Lean (Mathlib), theorem tsum_geometric_of_lt_one. See it on the map - The fundamental theorem of calculus: the integral of a derivative is the change in the original function
intervalIntegral.integral_eq_sub_of_hasDerivAt.{u_3} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E} (hderiv : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' MeasureTheory.volume a b) : ∫ (y : ℝ) in a..b, f' y = f b - f a Checked by Lean (Mathlib), theorem intervalIntegral.integral_eq_sub_of_hasDerivAt. See it on the map - Rolle's theorem: a smooth curve that starts and ends at the same height is flat somewhere in between
exists_deriv_eq_zero {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfI : f a = f b) : ∃ c ∈ Set.Ioo a b, deriv f c = 0 Checked by Lean (Mathlib), theorem exists_deriv_eq_zero. See it on the map - The Schroeder-Bernstein theorem: if each of two sets fits one-to-one inside the other, they are the same size
Function.Embedding.schroeder_bernstein.{u, v} {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hf : Function.Injective f) (hg : Function.Injective g) : ∃ h, Function.Bijective h Checked by Lean (Mathlib), theorem Function.Embedding.schroeder_bernstein. See it on the map - The Banach fixed point theorem: a map that always pulls points closer together has a point it leaves where it is
ContractingWith.fixedPoint_isFixedPt.{u_1} {α : Type u_1} [MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [Nonempty α] [CompleteSpace α] : Function.IsFixedPt f (ContractingWith.fixedPoint f hf) Checked by Lean (Mathlib), theorem ContractingWith.fixedPoint_isFixedPt. See it on the map - The halting problem: no program can decide, for every program, whether it eventually stops
ComputablePred.halting_problem (n : ℕ) : ¬ComputablePred fun c => (c.eval n).Dom Checked by Lean (Mathlib), theorem ComputablePred.halting_problem. See it on the map - Dirichlet's approximation theorem: every real number is close to a fraction with a small bottom
Real.exists_int_int_abs_mul_sub_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) : ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1) Checked by Lean (Mathlib), theorem Real.exists_int_int_abs_mul_sub_le. See it on the map - There are exactly as many real numbers as there are sets of whole numbers
Cardinal.mk_real : Cardinal.mk ℝ = Cardinal.continuum Checked by Lean (Mathlib), theorem Cardinal.mk_real. See it on the map - For every real number x, 1 + x is at most e to the power x
Real.add_one_le_exp (x : ℝ) : x + 1 ≤ Real.exp x Checked by Lean (Mathlib), theorem Real.add_one_le_exp. See it on the map - Bernoulli's inequality: (1 + x) to the power n is at least 1 + n times x
one_add_mul_le_pow.{u_1} {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} (H : -2 ≤ a) (n : ℕ) : 1 + ↑n * a ≤ (1 + a) ^ n Checked by Lean (Mathlib), theorem one_add_mul_le_pow. See it on the map - The triangle inequality: the length of a sum is at most the sum of the lengths
norm_add_le.{u_4} {E : Type u_4} [SeminormedAddGroup E] (a b : E) : ‖a + b‖ ≤ ‖a‖ + ‖b‖ Checked by Lean (Mathlib), theorem norm_add_le. See it on the map - The weighted mean inequality: a geometric mean is never more than the arithmetic mean
Real.geom_mean_le_arith_mean2_weighted {w₁ w₂ p₁ p₂ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂) (hp₁ : 0 ≤ p₁) (hp₂ : 0 ≤ p₂) (hw : w₁ + w₂ = 1) : p₁ ^ w₁ * p₂ ^ w₂ ≤ w₁ * p₁ + w₂ * p₂ Checked by Lean (Mathlib), theorem Real.geom_mean_le_arith_mean2_weighted. See it on the map - A triangle's three angles add up to 180 degrees (pi)
EuclideanGeometry.angle_add_angle_add_angle_eq_pi.{u_1, u_2} {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ : P} (p₃ : P) (h : p₂ ≠ p₁) : EuclideanGeometry.angle p₁ p₂ p₃ + EuclideanGeometry.angle p₂ p₃ p₁ + EuclideanGeometry.angle p₃ p₁ p₂ = Real.pi Checked by Lean (Mathlib), theorem EuclideanGeometry.angle_add_angle_add_angle_eq_pi. See it on the map - Every Pythagorean triple comes from one formula (Euclid)
PythagoreanTriple.classification {x y z : ℤ} : PythagoreanTriple x y z ↔ ∃ k m n, (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)) Checked by Lean (Mathlib), theorem PythagoreanTriple.classification. See it on the map - Cauchy's theorem: a finite group has an element of order p for every prime p dividing its size
exists_prime_orderOf_dvd_card.{u_3} {G : Type u_3} [Group G] [Fintype G] (p : ℕ) [hp : Fact (Nat.Prime p)] (hdvd : p ∣ Fintype.card G) : ∃ x, orderOf x = p Checked by Lean (Mathlib), theorem exists_prime_orderOf_dvd_card. See it on the map - Counting two sets: the union plus the overlap equals the two sizes added
Finset.card_union_add_card_inter.{u_1} {α : Type u_1} [DecidableEq α] (s t : Finset α) : (s ∪ t).card + (s ∩ t).card = s.card + t.card Checked by Lean (Mathlib), theorem Finset.card_union_add_card_inter. See it on the map - The number of ways to shuffle so nothing stays in place follows the derangement formula
card_derangements_eq_numDerangements.{u_2} (α : Type u_2) [Fintype α] [DecidableEq α] : Fintype.card ↑(derangements α) = numDerangements (Fintype.card α) Checked by Lean (Mathlib), theorem card_derangements_eq_numDerangements. See it on the map - Hall's marriage theorem
Finset.all_card_le_biUnion_card_iff_exists_injective.{u, v} {ι : Type u} {α : Type v} [DecidableEq α] (t : ι → Finset α) : (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x Checked by Lean (Mathlib), theorem Finset.all_card_le_biUnion_card_iff_exists_injective. See it on the map - Bolzano-Weierstrass: every bounded sequence has a convergent subsequence
tendsto_subseq_of_bounded.{u_1} {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : Bornology.IsBounded s) {x : ℕ → X} (hx : ∀ (n : ℕ), x n ∈ s) : ∃ a ∈ closure s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a) Checked by Lean (Mathlib), theorem tendsto_subseq_of_bounded. See it on the map - e to any real power is always positive
Real.exp_pos (x : ℝ) : 0 < Real.exp x Checked by Lean (Mathlib), theorem Real.exp_pos. See it on the map - The log of a product is the sum of the logs
Real.log_mul {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) : Real.log (x * y) = Real.log x + Real.log y Checked by Lean (Mathlib), theorem Real.log_mul. See it on the map - The fundamental theorem of arithmetic: a number breaks into primes in only one way
UniqueFactorizationMonoid.factors_unique.{u_1} {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {f g : Multiset α} (hf : ∀ x ∈ f, Irreducible x) (hg : ∀ x ∈ g, Irreducible x) (h : Associated f.prod g.prod) : Multiset.Rel Associated f g Checked by Lean (Mathlib), theorem UniqueFactorizationMonoid.factors_unique. See it on the map - 2^31 - 1 = 2,147,483,647
2^31 - 1 = 2147483647 Checked by the browser checker (the numbers only). See it on the map - 2^31 - 1 is prime
2^31 - 1 is prime Checked by the browser checker (the numbers only). See it on the map - 31 is prime
31 is prime Checked by the browser checker (the numbers only). See it on the map - 2^11 - 1 = 2047
2^11 - 1 = 2047 Checked by the browser checker (the numbers only). See it on the map - 2047 = 23 × 89
23 * 89 = 2047 Checked by the browser checker (the numbers only). See it on the map - 2047 is not prime (2^11 - 1 fails)
2047 is not prime Checked by the browser checker (the numbers only). See it on the map - The square root of 2^31 - 1 is about 46,341
2147483647^(1/2) ~= 46341 Checked by the browser checker (the numbers only). See it on the map - 2^100 is bigger (than 10^30)
2^100 > 10^30 Checked by the browser checker (the numbers only). See it on the map - 2^10 = 1024
2^10 = 1024 Checked by the browser checker (the numbers only). See it on the map - 1024 is slightly more than 10^3
2^10 > 10^3 Checked by the browser checker (the numbers only). See it on the map - 2^100 = (2^10)^10
2^100 = (2^10)^10 Checked by the browser checker (the numbers only). See it on the map - (2^10)^10 > (10^3)^10
(2^10)^10 > (10^3)^10 Checked by the browser checker (the numbers only). See it on the map - (10^3)^10 = 10^30
(10^3)^10 = 10^30 Checked by the browser checker (the numbers only). See it on the map - 2^100 ≈ 1.2677 × 10^30
2^100 ~= 1.2677 * 10^30 Checked by the browser checker (the numbers only). See it on the map - 2^100 exceeds 10^30 by about 27%
(2^100 - 10^30) / 10^30 ~= 0.27 Checked by the browser checker (the numbers only). See it on the map
Quarks (2)
- Two up quarks and one down quark give the proton its charge of exactly +1
2/3 + 2/3 - 1/3 = 1 Checked by the browser checker (the numbers only). See it on the map - One up quark and two down quarks give the neutron a charge of exactly 0
2/3 - 1/3 - 1/3 = 0 Checked by the browser checker (the numbers only). See it on the map
Atoms (1)
- 100 °C is 212 °F
(100 * 9 / 5) + 32 = 212 Checked by the browser checker (the numbers only). See it on the map
Cells (1)
- ODE: logistic growth from 10 toward a cap of 100 after 2 days
50 Checked by Lean, theorem CalculusLane.p97_logistic. See it on the map
People (36)
- Dice odds: sum of two dice is 7
1/6 Checked by Lean, theorem p01_dice_sum_seven. See it on the map - Coin streaks: a run of 5 heads in 20 flips
32751/131072 Checked by Lean, theorem p02_coin_streaks. See it on the map - Card draws: exactly two aces in five cards
2162/54145 Checked by Lean, theorem CheapLane.p04_two_aces_in_five. See it on the map - Birthday problem: a shared birthday among 23 people
1 - (365*364*363*...*343)/365^23 Checked by Lean, theorem TowerBatch.p05_birthday_problem. See it on the map - Random walk: return to origin after 20 steps
46189/262144 Checked by Lean, theorem p06_random_walk. See it on the map - Monty Hall: win probability when switching
2/3 Checked by Lean, theorem p07_monty_hall. See it on the map - Waiting for a six: expected rolls to first 6
6 rolls Checked by Lean, theorem WaitingLane.p09_rolls_to_first_six. See it on the map - Maximum of two dice: expected larger face
161/36 Checked by Lean, theorem p10_max_of_two_dice. See it on the map - Three or more sixes in ten rolls
566299/2519424 Checked by Lean, theorem CheapLane.p12_three_plus_sixes. See it on the map - Expected cards to the first ace
53/5 cards Checked by Lean, theorem TowerBatch.p13_cards_to_first_ace. See it on the map - Three-of-five vote: chance of passing at 60% yes
2133/3125 Checked by Lean, theorem TowerBatch.p17_three_of_five_vote. See it on the map - St. Petersburg payout capped at 2^20
21 dollars Checked by Lean, theorem TowerBatch.p22_st_petersburg_capped. See it on the map - Markov weather: rain exactly four steps after a sunny start
2137/10000 Checked by Lean, theorem p31_markov_weather_four_steps. See it on the map - Birthdays: expected number of different days among 30 people
5840637997733944304472717260382885356354745452713098221901782271034552207449/202531728519726872798204574491055504334773427222006304748356342315673828125 Checked by Lean, theorem CheapLane.p36_birthday_expected_distinct. See it on the map - Random walk: first return to the start exactly at step 10
7/256 Checked by Lean, theorem CheapLane.p40_first_return_10. See it on the map - Shuffle: no card back in its place among 10 cards
16481/44800 Checked by Lean, theorem p41_shuffle_derangement_ten. See it on the map - Shuffle: expected number of cycles in a shuffled pack of 20
55835135/15519504 Checked by Lean, theorem CheapLane.p42_shuffle_expected_cycles. See it on the map - Shuffle: some originally neighbouring pair stays together in order
2160343/3628800 Checked by Lean, theorem CheapLane.p43_shuffle_kept_neighbours. See it on the map - Cards: a 13-card hand with no spades but every other suit present
8091223647/635013559600 Checked by Lean, theorem CheapLane.p44_bridge_hand_no_spades. See it on the map - Cards: all four aces appear before any king in a shuffled deck
1/70 Checked by Lean, theorem CheapLane.p45_aces_before_kings. See it on the map - Polya urn: exactly three reds in five draws
4/21 Checked by Lean, theorem CheapLane.p49_polya_three_reds. See it on the map - Birthdays: expected number of same-birthday pairs among 28 people
378/365 pairs Checked by Lean, theorem CheapLane.p53_birthday_expected_pairs. See it on the map - expected value of a wide lognormal payout
exp(2) Checked by Lean, theorem WaitingLane.p56_lognormal_mean. See it on the map - A 13-card hand from a shuffled deck holds all four aces and all four kings
11/6431950 Checked by Lean, theorem TowerBatch.p65_trap_bridge_aces_kings. See it on the map - chance of disease after a positive 99%-sensitive test
11/122 Checked by Lean, theorem TowerBatch.p65_trap_medical_test_positive. See it on the map - all five backup units fail, with a rare common shock
10000000999/10000000000000 Checked by Lean, theorem TowerBatch.p68_trap_common_shock_failure. See it on the map - Twenty fair dice total 30 or less
9944165/1218719480020992 Checked by Lean, theorem TowerBatch.p69_trap_twenty_dice_low_tail. See it on the map - days 100 and 101 are both rainfall records
1/10100 Checked by Lean, theorem TowerBatch.p69_trap_two_records_in_row. See it on the map - Floating block: submerged depth of a wooden block
3/10 m Checked by Lean, theorem PhysicsLane.p83_floating_block_depth. See it on the map - Elastic collision: speed of the 2 kg cart after a head-on hit
1 m/s Checked by Lean, theorem PhysicsLane.p88_elastic_two_kg_cart. See it on the map - Roast an unstuffed 12 lb turkey at 325°F (163°C)
(325 - 32) * 5 / 9 ~= 163 Checked by the browser checker (the numbers only). See it on the map - The time is only a guide; the turkey is done when a meat thermometer reads 165°F (74°C)
(165 - 32) * 5 / 9 ~= 74 Checked by the browser checker (the numbers only). See it on the map - 2.7 liters is roughly 11 cups
2.7 / 0.2365882365 ~= 11 Checked by the browser checker (the numbers only). See it on the map - With annual compounding, $10,000 at 7% for 10 years grows to about $19,671.51
10000 * 1.07^10 ~= 19671.51 Checked by the browser checker (the numbers only). See it on the map - That's a gain of roughly $9,672
19671.51 - 10000 ~= 9672 Checked by the browser checker (the numbers only). See it on the map - If interest compounds monthly instead, you'd end up with about $20,097
10000 * (1 + 0.07 / 12)^120 ~= 20097 Checked by the browser checker (the numbers only). See it on the map
Worlds (11)
- 8,848.86 meters is 29,031.7 feet
8848.86 / 0.3048 ~= 29031.7 Checked by the browser checker (the numbers only). See it on the map - 65 mph × 3.5 hours = 227.5 miles
65 * 3.5 = 227.5 Checked by the browser checker (the numbers only). See it on the map - 227.5 miles is about 366.1 kilometers
227.5 * 1.609344 ~= 366.1 Checked by the browser checker (the numbers only). See it on the map - A day has 86,400 seconds
86400 = 24 * 60 * 60 Checked by the browser checker (the numbers only). See it on the map - 24 × 60 × 60 equals 86,400
24 * 60 * 60 = 86400 Checked by the browser checker (the numbers only). See it on the map - A standard 365-day year has 31,536,000 seconds
365 * 86400 = 31536000 Checked by the browser checker (the numbers only). See it on the map - A leap year (366 days) has 31,622,400 seconds
366 * 86400 = 31622400 Checked by the browser checker (the numbers only). See it on the map - The Gregorian calendar year works out to about 31,556,952 seconds
365.2425 * 86400 ~= 31556952 Checked by the browser checker (the numbers only). See it on the map - roughly 64 million square miles
165000000 / 1.609344^2 ~= 64000000 Checked by the browser checker (the numbers only). See it on the map - 4,000 meters is about 13,000 feet
4000 / 0.3048 ~= 13000 Checked by the browser checker (the numbers only). See it on the map - 11,000 meters is about 36,000 feet
11000 / 0.3048 ~= 36000 Checked by the browser checker (the numbers only). See it on the map
Stars (11)
- 299,792,458 m/s is about 300,000 km/s
c / 1000 ~= 300000 Checked by the browser checker (the numbers only). See it on the map - that is about 186,282 miles/s
c / mile ~= 186282 Checked by the browser checker (the numbers only). See it on the map - light takes roughly 1.3 seconds to get from the Moon to us
384400000 / c ~= 1.3 Checked by the browser checker (the numbers only). See it on the map - The Sun is about 149.6 million kilometers from Earth on average
au / 1000 ~= 149600000 Checked by the browser checker (the numbers only). See it on the map - The Sun is about 93 million miles from Earth on average
au / mile ~= 93000000 Checked by the browser checker (the numbers only). See it on the map - 343 m/s is roughly 1,235 km/h
343 * 3.6 ~= 1235 Checked by the browser checker (the numbers only). See it on the map - 343 m/s is roughly 767 mph
343 * 3600 / 1609.344 ~= 767 Checked by the browser checker (the numbers only). See it on the map - Every 3 seconds of delay is about 1 kilometer
1000 / 343 ~= 3 Checked by the browser checker (the numbers only). See it on the map - Every 5 seconds of delay is about 1 mile
mile / 343 ~= 5 Checked by the browser checker (the numbers only). See it on the map - A 5-second delay puts the lightning about 1.7 km away
5 * 343 / 1000 ~= 1.7 Checked by the browser checker (the numbers only). See it on the map - A 5-second delay is roughly 1 mile away
5 * 343 / mile ~= 1 Checked by the browser checker (the numbers only). See it on the map
Galaxies (1)
- A light-year, the ruler for galaxies, is exactly 9,460,730,472,580,800 meters
c * year = 9460730472580800 Checked by the browser checker (the numbers only). See it on the map
The observable universe (2)
- A parsec, the ruler for the universe, is about 3.26 light-years
au * 648000 / pi / lightyear ~= 3.26 Checked by the browser checker (the numbers only). See it on the map - Light takes about 499 seconds, a little over 8 minutes, to cross one astronomical unit
au / c ~= 499 Checked by the browser checker (the numbers only). See it on the map