Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
This lecture introduces Coq, a proof assistant, focusing on the theorem and_comm, which states that for all propositions P and Q, if P and Q are true, then Q and P are also true. The lecture covers the process of proving this theorem step by step using Coq's proof assistant.