Learn Lean 4 programming language & proof assistant

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 to August 23 in ILSB 233, as well as online for those not able to attend in person.

Please reach out to Prof. Tyler Josephson (CBEE) to learn more! tjo@umbc.edu