Classic mathematics

The quadratic equation

Discover the algebra behind the quadratic formula, then prove exactly which integers solve x²−5x+6=0.

-- The quadratic equation
-- History: c. 1700 BCE · Babylonian quadratic problems.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Completing the square explains why the discriminant b²−4ac appears.
-- Scope: Proves the completed-square identity and its equivalence to being a root when a≠0, over integers. The real square-root formula needs a larger number library.
-- Source: https://mathshistory.st-andrews.ac.uk/HistTopics/Quadratic_etc_equations/

theorem completing_square (a b c x : Int) :
    (2*a*x+b)^2 - (b^2-4*a*c) = 4*a*(a*x^2+b*x+c) := by
  grind

theorem quadratic_criterion (a b c x : Int) (ha : a ≠ 0) :
    a*x^2+b*x+c = 0 ↔ (2*a*x+b)^2 = b^2-4*a*c := by
  constructor
  · intro h
    grind
  · intro h
    have product : (4*a)*(a*x^2+b*x+c) = 0 := by grind
    rcases Int.mul_eq_zero.mp product with hz | hz
    · have : a = 0 := by omega
      exact False.elim (ha this)
    · exact hz

theorem roots (x : Int) : x^2-5*x+6=0 ↔ x=2 ∨ x=3 := by
  constructor
  · intro h
    have product : (x-2)*(x-3) = 0 := by grind
    rcases Int.mul_eq_zero.mp product with h2 | h3
    · left; omega
    · right; omega
  · intro h
    rcases h with h2 | h3 <;> grind

Explanation

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Change the last equation to x²−7x+12=0 and identify its two roots.