ex quod libet

Stream: Lean for teaching

[Patrick Massot]

I'm marking the exam of the course where I used Lean. A student invoked the "ex quod libet" principle. I guess it means that from nothing they can derive whatever they want. It sounds efficient.

[Mario Carneiro]

Yes, it seems to be quite the groundbreaking principle. See also http://inutile.club/estatis/falso/

[Patrick Massot]

Indeed, I thought about that link

[Patrick Massot]

I came very close to concluding that I should use LaTeX instead of Lean as my teaching software, because I saw a huge correlation between students who typed their exam using LaTeX and the exam quality. But I've found a counter-example.

[Jeremy Avigad]

Correlation ~= causality!

[Patrick Massot]

Of course!