Number theory
Pell’s equation: a next solution
Turn one integer solution into another, and prove the transformation preserves the equation.
Open Pell.lean in editor-- Top 100 #39: Pell’s equation: a next solution
-- History: 1759 · Euler milestone in the list.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Starting at (3,2), the recurrence gives (17,12), then (99,70).
-- Scope: Proves that the displayed recurrence preserves x² − 2y² = 1. It does not classify all Pell solutions.
-- Source: https://lurch.plus/100/
theorem pell_step (x y : Int) (h : x^2 - 2*y^2 = 1) :
(3*x+4*y)^2 - 2*(2*x+3*y)^2 = 1 := by
grind
example : (3 : Int)^2 - 2*2^2 = 1 := by decide
example : (17 : Int)^2 - 2*12^2 = 1 := by decide
Explanation
theorem / example
A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.
grind
Combines logical reasoning and polynomial normalization to construct a proof term that Lean checks.
Int
Exact integers, including negatives. Unlike Nat subtraction, integer subtraction does not truncate at zero.
Background and proof scope
1759 · Euler milestone in the list
Starting at (3,2), the recurrence gives (17,12), then (99,70).
Proves that the displayed recurrence preserves x² − 2y² = 1. It does not classify all Pell solutions.
Historical Top 100 list (reproduced by Lurch)Expected output
Reference only. Run the file to check its actual result.
File checked successfully.
Exercise
Write main to print five steps of this recurrence.