AI‑for‑Math Starter Kit — Tools & Workflow

Open-source software, AI systems, and a compact workflow you can use to start applying technology to research-level math.

Top tools (quick reference)

L4

Lean (Lean 4)

Proof assistant — formalize theorems and produce machine-checked proofs. Excellent community math library (mathlib).

Website
IS

Isabelle/HOL

Interactive theorem prover with strong automation and long maturity in formal logic.

Website
CO

Coq

Foundational proof assistant used in many formalization projects and research areas.

Website
Z3

Z3 (SMT solver)

Automated reasoning engine for satisfiability modulo theories — useful for lemmas and constraint solving.