Complex numbers? Intermediate Value Theorem?

As far as I know, neither the complex numbers nor the intermediate value theorem are in Lean. On the other hand, the real numbers, plus all the facts about them that we need, are there, as long as we install the mathlib library. So I think it’s about time today that we figure out how to get mathlib running on the machines in the MLC. Once the bleeding edge versions of Lean and Mathlib are up and running, we can do things like this:

``` import analysis.real structure complex : Type := (re : ℝ) (im : ℝ) notation `ℂ` := complex namespace complex -- "coercion" from reals to complexes: def of_real (r : ℝ) : ℂ := { re := r, im := 0} instance : has_zero ℂ := ⟨of_real 0⟩ instance : has_one ℂ := ⟨of_real 1⟩ instance : has_coe ℝ ℂ := ⟨of_real⟩ -- define addition and multiplication etc here! end complex ```

Can we prove that the complex numbers form a field? What does one have to do to prove this? We can take a look and find out.

At some point I feel like we’ll need to take the norm of a complex number, but I wrote a square root function so we can use this.

On the other hand, it would probably be better to prove that a positive real has a positive real $n$‘th root for all $n$, and as far as I know that isn’t in Lean either. It would follow from the intermediate value theorem, which as far as I know isn’t there either — but the notion of a continuous function is there! So we could try and prove the intermediate value theorem. Or figure out if it’s there already…

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in Uncategorized. Bookmark the permalink.

2 Responses to Complex numbers? Intermediate Value Theorem?

1. You may want to see https://en.wikipedia.org/wiki/Constructive_analysis#The_intermediate_value_theorem. Afaik the IVT fails to hold in Lean

Like

• xenaproject says:

Brendan, my understanding is that you’re saying that IVT fails in constructive mathematics. But Lean has non-constructive axioms, for example classical.choice. The IVT should be provable in Lean no problem — what will happen though is that if you type “#print axioms IVT” after you proved it, it will output (at least) “classical.choice”. As far as I am concerned this is not remotely a problem, because as long as I am using Lean in some way which is embeddable into ZFC + existence of arbitrarily large inaccessible cardinals (which is where most modern mathematics takes place in real life) then this is acceptable to me.

Like