Sqrt 2

Description

Prove 'Square root of two is irrational'.

Theorem (download)

module Theorem where

open import Data.Nat
open import Relation.Binary.PropositionalEquality using (_≡_)

postulate
  sqrt2 : (n m : ℕ) → n * n ≡ 2 * m * m → m ≡ 0

Verifier

module Verifier where

open import Data.Nat
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Theorem

verify : (n m : ℕ) → n * n ≡ 2 * m * m → m ≡ 0
verify = sqrt2

Proofs

Rank Prover Size Date
1 notogawa 2728 2013-08-29 00:06:55 JST
2 trigott 4728 2017-07-08 10:58:15 JST
3 Rotsor 5255 2014-04-21 05:16:20 JST