A Noncomputable function

An interesting example of a non-constructive proof is the following:

Theorem: There exist irrational numbers $a$ and $b$ such that $a^b$ is rational. Proof: Let b = √2. If b^b is rational, then we can take a = b. Otherwise, we can take a = √2^{√2}, so a^b=2.

We can prove this in Lean. But a function that returns such a pair of numbers has to be defined as noncomputable in Lean.

@[reducible, inline]

noncomputable abbrev sqrt2 : ℝ

The square root of 2 (an abbreviation).

Equations

• sqrt2 = √2

theorem sq_sq_sq_sqrt2_rational : (sqrt2 ^ sqrt2) ^ sqrt2 = 2

The equation (sqrt2^sqrt2)^sqrt2 = 2.

theorem irrational_power_irrational_rational : ∃ (a : ℝ) (b : ℝ), Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)

There exists an irrational numbers a and b such that a^b is rational.

structure IrrationalPair : Type

A structure that contains irrational numbers a and b such that a^b is rational along with proofs.

• a : ℝ
• b : ℝ
• irrational_a : Irrational self.a
• irrational_b : Irrational self.b
• rational_ab : ¬Irrational (self.a ^ self.b)

noncomputable def irrationalPair : IrrationalPair

Noncomputable function that returns an IrrationalPair, i.e., irrational numbers a and b such that a^b is rational.

Equations

• irrationalPair = Classical.choice irrationalPair.proof_1

noncomputable def irrationalPair' : { ab : ℝ × ℝ // Irrational ab.1 ∧ Irrational ab.2 ∧ ¬Irrational (ab.1 ^ ab.2) }

A noncomputable function that returns an IrrationalPair, i.e., irrational numbers a and b such that a^b is rational, represented as a subtype.

Equations

• irrationalPair' = Classical.choice irrationalPair'.proof_1