Chapter 1: Misformalisations

[pitmonticone]

The following theorems were negated by @Aristotle-Harmonic:

• infinitely_many_more_proofs

More specifically:

import Mathlib
open Lean Meta Elab Tactic in
elab "revert_all" : tactic => do
  let goals ← getGoals
  let mut newGoals : List MVarId := []
  for mvarId in goals do
    newGoals := newGoals.append [(← mvarId.revertAll)]
  setGoals newGoals

open Lean.Elab.Tactic in
macro "negate_state" : tactic => `(tactic|
  (
    guard_goal_nums 1
    revert_all
    refine @(((by admit) : ∀ {p : Prop}, ¬p → p) ?_)
    try (push_neg; guard_goal_nums 1)
  )
)

noncomputable section AristotleLemmas

lemma counterexample_infinity_primes : ∃ S : ℕ → ℤ, AlmostInjective S ∧ Asymptotics.ofSubexponentialGrowth S ∧ {p : Nat.Primes | ∃ n : ℕ, (p : ℤ) ∣ S n}.Infinite := by
  refine' ⟨ fun n => n, _, _, _ ⟩ <;> norm_num [ AlmostInjective ];
  · use 1;
  · refine' ⟨ fun n => Nat.log 2 ( Nat.log 2 n ) + 2, fun n => ⟨ _, _ ⟩ ⟩ <;> norm_num [ Real.rpow_natCast ];
    · norm_cast;
      have := Nat.lt_pow_succ_log_self ( by decide : 1 < 2 ) ( Nat.log 2 n );
      rw [ Nat.pow_succ ] at this;
      exact le_trans ( Nat.le_of_lt ( Nat.lt_pow_succ_log_self ( by decide ) _ ) ) ( Nat.pow_le_pow_right ( by decide ) ( by ring_nf at *; linarith ) );
    · -- We'll use that $Nat.log 2 (Nat.log 2 n)$ grows much slower than $Nat.log 2 n$.
      have h_log_log : Filter.Tendsto (fun n => (Nat.log 2 (Nat.log 2 n) : ℝ) / (Nat.log 2 n : ℝ)) Filter.atTop (𝓝 0) := by
        -- We'll use the fact that $\log_2(\log_2(n))$ grows much slower than $\log_2(n)$.
        have h_log_log : Filter.Tendsto (fun x : ℕ => (Nat.log 2 x : ℝ) / x) Filter.atTop (nhds 0) := by
          -- We can convert this limit into a form that is easier to handle by substituting $y = \log_2 x$.
          suffices h_log : Filter.Tendsto (fun y : ℕ => (y : ℝ) / 2 ^ y) Filter.atTop (nhds 0) by
            have h_log : Filter.Tendsto (fun x : ℕ => (Nat.log 2 x : ℝ) / 2 ^ (Nat.log 2 x)) Filter.atTop (nhds 0) := by
              exact h_log.comp ( Filter.tendsto_atTop_atTop.mpr fun y => ⟨ 2 ^ y, fun x hx => Nat.le_log_of_pow_le ( by norm_num ) hx ⟩ );
            refine' squeeze_zero_norm' _ h_log;
            filter_upwards [ Filter.eventually_gt_atTop 1 ] with x hx using by rw [ Real.norm_of_nonneg ( by positivity ) ] ; gcongr ; norm_cast ; exact Nat.pow_log_le_self 2 <| by linarith;
          refine' squeeze_zero_norm' _ tendsto_inverse_atTop_nhds_zero_nat;
          norm_num;
          exact ⟨ 8, fun n hn => by rw [ inv_eq_one_div, div_le_div_iff₀ ] <;> norm_cast <;> induction hn <;> norm_num [ Nat.pow_succ ] at * ; nlinarith ⟩;
        exact h_log_log.comp ( Filter.tendsto_atTop_atTop.mpr fun x => ⟨ 2 ^ x, fun n hn => Nat.le_log_of_pow_le ( by norm_num ) hn ⟩ );
      -- We can use the fact that addition is continuous to combine the limits.
      have h_add : Filter.Tendsto (fun n => ((Nat.log 2 (Nat.log 2 n) : ℝ) / (Nat.log 2 n : ℝ)) + (2 / (Nat.log 2 n : ℝ))) Filter.atTop (𝓝 (0 + 0)) := by
        exact Filter.Tendsto.add h_log_log <| tendsto_const_nhds.div_atTop <| tendsto_natCast_atTop_atTop.comp <| Filter.tendsto_atTop_atTop.mpr fun x => ⟨ 2 ^ x, fun n hn => Nat.le_log_of_pow_le ( by norm_num ) hn ⟩;
      convert h_add using 2 ; norm_num [ add_div ];
      norm_num [ ← NNReal.tendsto_coe ];
  · exact Set.infinite_univ.mono fun p _ => ⟨ 0, by norm_num ⟩

lemma smooth_numbers_bound (P : Finset ℕ) :
  ∃ C : ℝ, ∀ N : ℕ, N > 0 →
  ((Finset.range (N + 1)).filter (fun n => n ∈ Nat.factoredNumbers P)).card ≤ C * (Nat.log 2 N + 1) ^ P.card := by
    by_contra h_contra;
    -- Define the set $S$ of natural numbers $n \leq N$ with all prime factors in $P$.
    set S := fun N : ℕ => Finset.filter (fun n => n ∈ Nat.factoredNumbers P) (Finset.range (N + 1));
    -- To prove the bound, we use the fact that the cardinality of $S$ is bounded by the product of the number of divisors of $N$ for each prime in $P$.
    have h_divisors : ∀ N > 0, (S N).card ≤ (∏ p ∈ P, (Nat.log p N + 1)) := by
      -- Each number $n \in S$ can be written as $n = \prod_{p \in P} p^{e_p}$ where $0 \leq e_p \leq \log_p N$.
      intros N hN_pos
      have h_factorization : ∀ n ∈ S N, ∃ e : ℕ → ℕ, (∀ p ∈ P, e p ≤ Nat.log p N) ∧ n = ∏ p ∈ P, p ^ e p := by
        intro n hn
        rw [Finset.mem_filter] at hn
        obtain ⟨hn_range, hn_factored⟩ := hn
        rw [Nat.mem_factoredNumbers] at hn_factored
        obtain ⟨hn_pos, hn_prime_factors⟩ := hn_factored;
        refine' ⟨ fun p => Nat.factorization n p, _, _ ⟩;
        · intro p hp;
          by_cases hp_prime : Nat.Prime p;
          · exact Nat.le_log_of_pow_le hp_prime.one_lt <| Nat.le_trans ( Nat.le_of_dvd ( Nat.pos_of_ne_zero hn_pos ) <| Nat.ordProj_dvd _ _ ) <| Finset.mem_range_succ_iff.mp hn_range;
          · simp_all +decide [ Nat.factorization_eq_zero_of_non_prime ];
        · conv_lhs => rw [ ← Nat.factorization_prod_pow_eq_self hn_pos ] ;
          rw [ Finsupp.prod_of_support_subset ] <;> aesop_cat;
      choose! e he₁ he₂ using h_factorization;
      -- The number of possible exponents $e_p$ for each prime $p \in P$ is at most $\log_p N + 1$.
      have h_exponents : ∀ p ∈ P, Finset.card (Finset.image (fun n => e n p) (S N)) ≤ Nat.log p N + 1 := by
        exact fun p hp => le_trans ( Finset.card_le_card <| Finset.image_subset_iff.mpr fun n hn => Finset.mem_Icc.mpr ⟨ Nat.zero_le _, he₁ n hn p hp ⟩ ) ( by simpa );
      -- The number of possible combinations of exponents $e_p$ for each prime $p \in P$ is at most the product of the number of exponents for each prime.
      have h_combinations : Finset.card (Finset.image (fun n => (fun p => e n p) : ℕ → P → ℕ) (S N)) ≤ ∏ p ∈ P, (Nat.log p N + 1) := by
        have h_combinations : Finset.card (Finset.image (fun n => (fun p => e n p) : ℕ → P → ℕ) (S N)) ≤ Finset.card (Finset.pi P fun p => Finset.image (fun n => e n p) (S N)) := by
          refine' le_trans _ ( Finset.card_le_card _ );
          rotate_left;
          exact Finset.image ( fun n => fun p hp => e n p ) ( S N );
          · simp +decide [ Finset.subset_iff ];
            exact fun n hn p hp => ⟨ n, hn, rfl ⟩;
          · rw [ Finset.card_image_of_injOn, Finset.card_image_of_injOn ];
            · intro n hn m hm hnm;
              rw [ he₂ n hn, he₂ m hm ];
              exact Finset.prod_congr rfl fun p hp => congr_arg _ ( congr_fun ( congr_fun hnm p ) hp );
            · intros n hn m hm hnm;
              rw [ he₂ n hn, he₂ m hm ];
              exact Finset.prod_congr rfl fun p hp => congr_arg _ ( congr_fun hnm ⟨ p, hp ⟩ );
        exact h_combinations.trans ( by rw [ Finset.card_pi ] ; exact Finset.prod_le_prod' h_exponents );
      rwa [ Finset.card_image_of_injOn ] at h_combinations;
      intros n hn m hm hnm;
      rw [ he₂ n hn, he₂ m hm ];
      exact Finset.prod_congr rfl fun p hp => congr_arg _ ( congr_fun hnm ⟨ p, hp ⟩ );
    -- We'll use the fact that if the logarithm of a number is less than or equal to another number, then the number itself is less than or equal to the exponential of that number.
    have h_exp : ∀ N > 0, (∏ p ∈ P, (Nat.log p N + 1)) ≤ (∏ p ∈ P, ((Nat.log 2 N) + 1)) := by
      intro N hN_pos; refine Finset.prod_le_prod' fun p hp => ?_; rcases p with ( _ | _ | p ) <;> simp_all +decide [ Nat.log_of_lt ] ;
      gcongr ; linarith;
      linarith;
    simp +zetaDelta at *;
    exact h_contra 1 |> fun ⟨ N, hN₁, hN₂ ⟩ => hN₂.not_le <| by simpa using mod_cast le_trans ( h_divisors N hN₁ ) ( h_exp N hN₁ ) ;

end AristotleLemmas

theorem infinitely_many_more_proofs (S : ℕ → ℤ)
  (h₁ : AlmostInjective S) (h₂ : ofSubexponentialGrowth S) :
  {p : Nat.Primes | ∃ n : ℕ, (p : ℤ) ∣ S n}.Finite := by
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  -- Let's choose any sequence $S$ that satisfies the conditions.
  obtain ⟨S, hS⟩ := counterexample_infinity_primes; exact ⟨S, hS⟩;