Undergraduate CS2 -- Discrete Math and Theory -- In Lean

Stream: CSLib

[Kevin Sullivan]

FWIW, I've been trying to figure out how to teach undergraduate CS2, discrete math and theory, entirely using Lean (3 then 4) for some years now. You can find the always-a-WIP course notes, and an justification for the effort, at https://kevinsullivan.github.io/dmtl4. The notes are now quite a bit more than a ugrad class, as most (at least most UVa) grad students also have no sense of formal logic or mathematics and they too need to start from scratch. I've meant for ages to add a link to this course to the Lean 4 repo. Let me know if/how I might help. In addition to the course notes I can describe my experiences trying to do this over the years. If this isn't the right forum for this information, then please forgive and suggest a better one. Matt Dwyer suggested I join this discussion.

[Kevin Sullivan]

(deleted)

[Clark Barrett]

Thanks for sharing your notes! I do think this will be of interest to many who are also interested in CSLib and could even help provide some guidance for the CSLib effort.

[Kevin Sullivan]

Clark Barrett said:

Thanks for sharing your notes! I do think this will be of interest to many who are also interested in CSLib and could even help provide some guidance for the CSLib effort.

Happy to help any way I can. Just let me know.