proof of false

Stream: general

[Kenny Lau]

I've produced a proof of false in Lean by messing around with inductive types and universes and creating a type that is empty and inhabited in the same time. The whole file is 41 lines long and can be accessed by clicking this sentence.

[Kevin Buzzard]

Hey aren't you on something like UTC+8?