AI and Lean

Rutgers University, New Jersey, USA

October 8, 2025

Slides

The slides are available here: Jauslin_AIlean_2025.pdf

Links and resources

Installing and running Lean

• Live Lean server, to use Lean without having to install it: https://live.lean-lang.org
• Installation instructions: https://lean-lang.org/install/

Lean tutorials

• Learning Lean by practice with elementary number theory: Natural Number Game
• Learning Lean by practice with analysis (experimental): Real Analysis Game

Documentation

• Learning resources page: https://leanprover-community.github.io/learn.html
• Mathlib documentation: https://leanprover-community.github.io/mathlib4_docs/
• Lean Zulip chat: https://leanprover.zulipchat.com/