Load Theorema and Set Preferences

Needs["Theorema`"]

SetOptions[Prove, transformBy -> ProofSimplifier, 
        TransformerOptions -> {branches -> Proved, 
            steps -> Essential}];

The Proof of the Main Theorem

Theorem["sqrt[2] irrational", ¬ rat[(Sqrt[2])]]

Definition[\("rational", 
      any[r], 
rat[
          r] : \(\(⇔\)\(∃ \+\(a, b\)\((nat[a] ∧ 
                nat[b] ∧ \((r = a\/b)\) ∧ coprime[a, b])\)\)\)\)]

Definition[\("sqrt", 
      any[x], 
\@x := \(\(\(∍\)\(!\)\)\+y\) \((y\^2 = x)\)\)]

Lemma["coprime", any[a, b], 
      with[nat[a] ∧ 
          nat[b]], 
(2  (b^2) = 
            (a^2)) \[Implies] ¬ coprime[a, b]]

Prove[Theorem["sqrt[2] irrational"], 
        using -> ⟨Lemma["coprime"], 
            Definition["rational"], 
            Definition["sqrt"]⟩, 
        built–in -> ⟨Built–in["Rational \
Numbers"]⟩, by -> ElementaryReasoner, 
        ProverOptions -> {SimplifyFormula -> True, 
            RWCombine -> True}];

The Proof of the Auxiliary Lemma

The auxiliary Lemma "coprime" is a statement essentially about natural numbers. In the spirit of theory exploration we assume this lemma to be proven during an (earlier) exploration of the notion "coprime" within the universe of natural numbers. In this section, we show this phase of exploration of the natural numbers.

Lemma["coprime", 
      any[a, b], 
(2  (b^2) = 
            (a^2)) \[Implies] ¬ coprime[a, b]]

Definition[\("even", 
      any[a], 
is–even[
          a] : \(\(⇔\)\(∃ \+m\((a = 2  m)\)\)\)\)]

Proposition["even numbers",any[a, b],
({{(2  b = a) \[Implies] is–even[a], "characteristic"}, {is–even[(a^2)] \[Implies] is–even[a], "even square"}})]

Proposition["common factor", 
      any[a, b], 
¬ coprime[2  a, 2  b]]

Prove[Lemma["coprime"], 
        using -> ⟨Proposition["even numbers"], 
            Proposition["common factor"], 
            Definition["even"]⟩, 
        built–in -> ⟨Built–in["Natural \
Numbers"]⟩, by -> ElementaryReasoner, 
        ProverOptions -> {SimplifyFormula -> True}, 
        SearchDepth -> 40];