Chapter 5: Misformalisations

[pitmonticone]

The following theorems were negated by @Aristotle-Harmonic:

• fermat_little
• quadratic_reciprocity_1
• quadratic_reciprocity_2

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 fermat_little (a : ℤ): (a : ZMod p) ≠ 0 → a ^ (p - 1) = (-1 : ZMod p) := by
  let units_finset := (Finset.univ : Finset (ZMod p)).erase 0
  let image_finset := (units_finset).image (fun x : ZMod p => (a : ZMod p) * x)
  have : units_finset = image_finset := by sorry
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  -- Let's choose any odd prime $p$ and an integer $a$ such that $a \equiv 1 \pmod{p}$.
  use 3, by exact Fact.mk (by decide), 1
  simp +decide

theorem quadratic_reciprocity_1 (p q : ℕ) (hp : p ≠ 2) (hq : q ≠ 2)
  [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] :
  (legendre_sym p q) * (legendre_sym q p) = -1 ^ ((p-1) / 2 * (q - 1) / 2 ) :=
  by
    -- Wait, there's a mistake. We can actually prove the opposite.
    negate_state;
    -- Proof starts here:
    -- Let's choose any two odd primes, say $p = 3$ and $q = 5$.
    use 3, 5;
    -- We'll use that 3 and 5 are primes and that their Legendre symbols are -1.
    simp +decide [book.quadratic_reciprocity.legendre_sym]

theorem quadratic_reciprocity_2 (p q : ℕ) (hp : p ≠ 2) (hq : q ≠ 2)
  [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] :
  (legendre_sym p q) * (legendre_sym q p) = -1 ^ ((p-1) / 2 * (q - 1) / 2 ) := by
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  -- Let's choose $p = 3$ and $q = 3$.
  use 3, 3;
  -- We know that 3 is a prime number.
  simp +decide [book.quadratic_reciprocity.legendre_sym]