Zulip Chat Archive

Stream: Lean for teaching

Topic: ex quod libet

Patrick Massot (May 22 2020 at 20:34):

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 (May 22 2020 at 20:54):

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

Patrick Massot (May 22 2020 at 21:07):

Indeed, I thought about that link

Patrick Massot (May 22 2020 at 21:08):

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 (May 22 2020 at 22:02):

Correlation ~= causality!

Patrick Massot (May 22 2020 at 22:02):

Of course!

Last updated: Dec 20 2023 at 11:08 UTC