The University of Arizona
Please note that this event has ended!

A Brief Introduction to Lean

Data Research Training Group Seminar

A Brief Introduction to Lean
Series: Data Research Training Group Seminar
Location: Hybrid, Math 402/Online Math 402
Presenter: Joseph Ruiz and Kevin Lin

Abstract: In this RTG seminar we will be doing a demo of Lean4. Lean 4 is a programming language which verifies proofs written in the language lean4 and attempts to give assistance during the writing of proofs. Lean 4 is a significant improvement over Lean3 which puts its proof verification abilities on par with languages such as COQ. Will be using an online lean4 service https://lean.math.hhu.de/ to demo the system. We will be using the lean4 package mathlib4 to show its capability to prove more advanced theorems. If you would like to learn more about either of the projects see the following links. https://github.com/leanprover-community/mathlib4 https://github.com/leanprover/lean4

Zoom link: https://www.math.arizona.edu/~klin/rtg-zoom