Six Lines · Book XIV — Principia Orthogona

The most famous short proof in mathematics shows that √2 is irrational, and Hardy and Wright give it in six lines. In 2006 Freek Wiedijk had it proved in seventeen different proof assistants and admitted that none of them could simply read the six lines and check them. Reinhard Kahle took that as a question about the structure of a proof. This chapter answers it in miniature: the six lines, in Lean, one sentence at a time.

1 · The challenge

“We clearly are not yet there”

Kahle quotes Hardy and Wright: "If √2 is rational, then the equation a² = 2b² is soluble in integers a, b with (a, b) = 1. Hence a² is even, and therefore a is even. If a = 2c, then 4c² = 2b², 2c² = b², and b is also even, contrary to the hypothesis that (a, b) = 1." He then quotes Wiedijk: "Ideally, a computer should be able to take this text as input and check it for its correctness. We clearly are not yet there." Wiedijk's diagnosis is that the text "does not have enough detail". Kahle turns that around, quoting Dana Scott, who says machine proofs have too much and asks "What really is a proof?" CITED

2 · The six lines, in Lean

One sentence, one step

HardyWright.lean proves Hardy and Wright's statement over the natural numbers: a² = 2b² with (a, b) = 1 is impossible. Every step is tagged with the sentence it carries out. KERNEL-CHECKED

HW	Hardy & Wright	Lean
1	“the equation a² = 2b² is soluble in integers a, b with (a, b) = 1”	the hypotheses hab, h
2	“Hence a² is even,”	have ha2 : 2 ∣ a ^ 2 := ⟨b ^ 2, h⟩
3	“and therefore a is even.”	have ha : 2 ∣ a := Nat.prime_two.dvd_of_dvd_pow ha2
4	“If a = 2c, then 4c² = 2b², 2c² = b²,”	obtain ⟨c, rfl⟩ := ha have hc : b ^ 2 = 2 * c ^ 2 := by nlinarith [h]
5	“and b is also even,”	have hb : 2 ∣ b := Nat.prime_two.dvd_of_dvd_pow ⟨c ^ 2, hc⟩
6	“contrary to the hypothesis that (a, b) = 1.”	have h2b : Nat.Coprime 2 b := … exact (Nat.Prime.coprime_iff_not_dvd Nat.prime_two).1 h2b hb

The whole argument takes 7 lines and 52 tokens of Lean, against Hardy and Wright's 49 words. It follows the same order: no step reordered, none added that the text lacks. The kernel accepts it with only the three standard axioms. COMPUTED

So are we there?Partly. The structure Kahle asked for can be kept, sentence for sentence. The detail Wiedijk missed has not vanished, though. It sits in five named library facts (prime_two, dvd_of_dvd_pow, coprime_dvd_left, coprime_iff_not_dvd, dvd_mul_right) and one tactic (nlinarith), which checks the arithmetic of step 4 for us. Hardy and Wright's reader supplies the same facts from memory. Twenty years of Mathlib have made the library a reader of that kind. What Lean still cannot do is take the English sentence itself as input. The translation from sentence to step was done by hand, and that is the gap Chapter 2's FIRMA tries to close. MODEL

3 · How this fits the book

Chapter 1 proved a claim Syntactic Structures made without proof. Chapter 2 found this series keeps its recipes in the Lean and its assertions in the prose. Here the two meet: the proof is written once in prose and once in Lean, and every sentence is lined up with its step. That is the structure Kahle wanted to be able to exchange between provers. His own proposal is an XML format for it, which is not implemented here. OPEN

Not establishedWiedijk's The Seventeen Provers of the World (2006) is quoted only through Kahle and is not held. Hardy and Wright's book is not held either; its proof is quoted as Kahle gives it. The count of 49 words is taken from Kahle's rendering, whose PDF drops the radical signs and superscripts. WANTED

R. Kahle, "Towards the Structure of Mathematical Proof", CENTRIA and DM, FCT, Universidade Nova de Lisboa (research supported by FCT projects PTDC/FIL-FCI/109991/2009 and PTDC/MHC-FIL/5363/2012). Held.
G. H. Hardy & E. M. Wright, An Introduction to the Theory of Numbers, p.39f (as quoted by Kahle).
F. Wiedijk (ed.), The Seventeen Provers of the World, Springer LNAI 3600, 2006 (as quoted by Kahle).