# Zulip Chat Archive

## Stream: general

### Topic: how to prove excluded middle (video)

#### Thorsten Altenkirch (Sep 27 2020 at 14:10):

I gave a talk with live proofs in our fp lunch meeting last Friday using lean for the first time:

Sorry for the low level of automatisation but this is the style I am also using in my lecture. The main story is that you don't need to assume EM as an axiom but there is also some discussion about lean...

#### Pedro Minicz (Sep 27 2020 at 17:47):

Very interesting! This remembers me of the "stable propositions" exercise at the end of the negation chapter of *Programming Language Foundations in Agda*. Coincidentally, I have redone the exercise in Lean around a week ago (you can see it here).

#### Junyan Xu (Sep 28 2020 at 05:12):

Coincidentally I also did some similar exercises regarding stable propositions (which corresponds to regular elements in Heyting algebras): https://gist.github.com/alreadydone/7474d5000c912194d794d06192e84f1e#file-choice_and_excluded_middle-lean-L557

Basically I formalized https://en.wikipedia.org/wiki/Heyting_algebra#The_De_Morgan_laws_in_a_Heyting_algebra in Lean.

Last updated: May 12 2021 at 05:19 UTC