This project is funded by Tenneessee AI Initiative
Organizer: Yulan Qing
Speaker: Kavindya Jayathilaka
Title: Introduction to LEAN programming
Abstract: Mathematical proofs are traditionally verified by human experts, leaving room for undetected errors. Lean 4 is a proof assistant that mechanically checks each logical step, enabling reliable formal verification. This talk provides a brief introduction to Lean 4 and Mathlib, the largest library of formally verified mathematics, highlighting its role in advancing rigorous computational reasoning and its growing relevance at the intersection of programming and mathematics.
What?
Formalization is the process of translating informal mathematics, logic, or scientific reasoning into a fully precise formal language, usually one that a computer proof assistant can check.
In mathematics, that often means:
writing definitions in a theorem prover such as Lean, Coq, Isabelle, or HOL
stating theorems in exact symbolic form
giving proofs step by step so the system can verify every inference
The goal is not just clarity for humans, but machine-checkable correctness.
Autoformalization is the process of doing some or all of that translation automatically, typically using AI or other automated methods.
Usually, autoformalization means converting things like:
textbook-style mathematical prose
handwritten or LaTeX proofs
informal theorem statements
into:
formal theorem statements
formal definitions
proof scripts in a proof assistant
A useful distinction is:
Formalization: a human or team writes the formal version.
Autoformalization: a system tries to generate the formal version from informal input.
Why?
make proofs more trustworthy
make advanced mathematics more searchable and reusable
support collaboration between humans and AI
accelerate the transition from informal insight to verified theorem
