Chapter 8: MIsformalisations

[pitmonticone]

The following theorems were negated by @Aristotle-Harmonic:

• lem_aux_i
• Theorem_3

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)
  )
)

lemma lem_aux_i (n : ℕ) (x : ℝ) : ∃ c : ℕ → ℤ, f_aux n x = ∑ i ∈ Icc n (2 * n), (c i) * x ^ i := by
  by_contra h_nonzero;
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  -- Let's choose `n = 2` and `x = 1/2`.
  use 2, 1 / 2;
  -- Let's simplify the expression for `f_aux 2 (1 / 2)`.
  simp [book.irrational.f_aux];
  -- Let's simplify the expression for `f_aux 2 (1 / 2)` further.
  intro x hx
  field_simp at hx;
  -- Simplify the right-hand side of the equation.
  norm_num [ Finset.sum_Ioc_succ_top, (Nat.succ_eq_succ ▸ Finset.Icc_succ_left_eq_Ioc) ] at hx;
  -- Simplify the equation $1 = 32 * ((x 2) / 4 + (x 3) / 8 + (x 4) / 16)$ to get a contradiction.
  field_simp at hx;
  -- Simplify the equation $512 = 32 * ((x 2 * 8 + 4 * x 3) * 16 + 4 * 8 * x 4)$ to get a contradiction.
  norm_cast at hx;
  grind

theorem Theorem_3 (n : ℕ) (h_n : n ≥ 3) : Irrational ( arccos (1 / (n : ℝ).sqrt) / π) := by
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  use 4; norm_num;
  -- We know that $\arccos(1/2) = \pi/3$.
  have h_arccos : Real.arccos (1 / 2) = Real.pi / 3 := by
    -- We know that $\cos(\pi/3) = 1/2$, so applying the arccos function to both sides gives us the result.
    rw [←Real.cos_pi_div_three, Real.arccos_cos] <;> linarith [Real.pi_pos];
  -- Substitute $\arccos(1/2) = \pi/3$ into the expression.
  rw [h_arccos];
  -- Simplify the expression $\frac{\pi}{3} / \pi$ to $\frac{1}{3}$.
  field_simp;
  -- Since $1/3$ is a rational number, it is not irrational.
  simp [book.irrational.Irrational];
  -- We know that $3^{-1} = \frac{1}{3}$, which is a rational number.
  use 1 / 3
  norm_num