Interested in learning to write computer-checked math proofs? Interested in learning an exciting new programming language?
Lean 4 is a new programming language that can be used to write code
that’s literally bug-free. It enables this because at its core, it is a proof
assistant that verifies math proofs. A global community of
mathematicians and computer scientists are building a database of
formally verified math proofs across the undergraduate curriculum, as
well as proofs at the frontiers of modern math.
This summer, an informal group of mathematicians, computer scientists,
physical scientists, and engineers at UMBC will be learning Lean 4.
Come join us – all are welcome!
We will meet weekly this summer from 1 – 3 pm EST on Wednesdays, June 28 – August 23 in ILSB 233.
Please reach out to Prof. Tyler Josephson (CBEE) to learn more! tjo@umbc. edu