Formalizing the future of mathematics.

Stanford AI for Lean is a student-led research community at Stanford focused on AI-assisted theorem proving, Lean 4, formal verification, and the future of trustworthy mathematical reasoning.

We bring together students and researchers who want to build the next generation of tools for verified mathematics and software. The group is closely connected to ongoing AI-for-formal-methods research in Prof. Sanmi Koyejo’s Stanford Trustworthy AI Research group, including work on Lean 4 benchmarks, autoformalization, formal proof search, and end-to-end verification of AI-generated code.

As of Spring 2026, the community has roughly 90 Discord members and regular weekly meetings of about 12-15 people. The core audience is Stanford students who want to read papers, learn Lean, build proof-assistant tooling, and collaborate on research at the intersection of AI, programming languages, mathematics, and verification.

Why This Matters

Modern AI systems are increasingly good at generating fluent text and code, but fluency is not the same as correctness. Formal verification offers a different standard: a proof either checks or it does not.

Lean 4 is becoming a central language for that future. It supports formal mathematics, verified software, proof automation, and machine-to-machine interfaces for AI theorem proving. The research question is no longer whether AI can produce convincing arguments. The question is whether AI can produce artifacts that withstand deterministic verification.

Stanford AI for Lean exists to train students and accelerate research in that direction.

Current Focus

  • AI-assisted theorem proving: using language models, search, and agentic workflows to help construct formal Lean proofs.
  • Autoformalization: translating informal mathematics, specifications, and software properties into formal Lean statements.
  • Verified code generation: building benchmarks and tools for checking whether AI-generated code satisfies precise formal specifications.
  • Trustworthy evaluation: designing contamination-resistant and verification-aware benchmarks for mathematical reasoning.
  • Lean infrastructure: improving interfaces, datasets, tutorials, and workflows that make Lean 4 useful to researchers and engineers.

Relevant Stanford-led work includes VeriBench, VeriBench-FTP, Pantograph, Putnam-AXIOM, and public writing on formal methods as scalable oversight.

Learning Resources

For students getting started with Lean, Brando maintains a public Learning the Lean 4 Interactive Theorem Prover tutorial playlist, with a companion learning_lean code repository and X announcement.

Contact

For collaborations or Stanford student participation, contact Brando Miranda at brando9 {at} stanford dot edu.

Useful links: