Number theory
Bézout: a gcd certificate
Negative coefficients let a linear combination of two positive integers equal 1. Supply a certificate Lean can check.
Open Bezout.lean in editor-- Top 100 #60: Bézout: a gcd certificate
-- History: Date unspecified in the list · Bézout.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: A linear combination supplies a compact certificate that a gcd is 1.
-- Scope: Proves the Bézout identity for 35 and 22 and checks their gcd. It does not construct coefficients for arbitrary inputs.
-- Source: https://lurch.plus/100/
-- 35*(-5) + 22*8 = 1.
theorem bezout_certificate :
∃ x y : Int, 35*x + 22*y = 1 := by
exact ⟨-5, 8, by decide⟩
example : Nat.gcd 35 22 = 1 := by decide
#eval (35 * (-5) + 22 * 8 : Int)
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.
decide
Builds a proof using a decision procedure. Here it checks a concrete arithmetic statement.
Int
Exact integers, including negatives. Unlike Nat subtraction, integer subtraction does not truncate at zero.
Background and proof scope
Date unspecified in the list · Bézout
A linear combination supplies a compact certificate that a gcd is 1.
Proves the Bézout identity for 35 and 22 and checks their gcd. It does not construct coefficients for arbitrary inputs.
Historical Top 100 list (reproduced by Lurch)Expected output
Reference only. Run the file to check its actual result.
1
Exercise
Find coefficients for 17 and 12. Can you use the Euclidean algorithm to produce them?