Awesome AI4Math

A curated list of AI for Mathematics resources — the ecosystem reshaping mathematics.

---

Contents

Core Technologies

• Proof Assistants
  • Dependent Type / HoTT — Lean, Coq, Agda, Idris, F*, Arend, Aya
  • HOL Family — Isabelle, HOL4, HOL Light
  • Other Important Systems — Mizar, Metamath, PVS, ACL2
  • Cubical Type Theory
  • Logical Frameworks
  • Historical Systems
  • Other / Emerging

AI & Automation

• AI for Formal Mathematics
  • Neural Theorem Provers — AlphaProof, Goedel, DeepSeek, Kimina
  • IDE & Copilot Tools — Mozi, Lean Copilot, llmstep
  • Search Engines — LeanSearch, Loogle
  • Infrastructure & Frameworks — LeanDojo, Pantograph
  • Benchmarks & Datasets — MiniF2F, PutnamBench
  • Autoformalization
  • Geometry Solvers — AlphaGeometry, Seed-Geometry
  • Agentic CLI Tools
• Automated Theorem Provers (Classical)
  • First-Order ATPs — Vampire, E Prover
  • SMT Solvers — Z3, CVC5
  • Integration with Proof Assistants

Ecosystem

• Companies & Organizations
  • AI Math Startups — Harmonic, Axiom, Math Inc., Morph
  • Research Organizations — Lean FRO, Numina
  • Academic Labs — PKU, Caltech, Princeton
  • Big Tech AI Labs — DeepMind, ByteDance, DeepSeek
  • Compute Infrastructure — Hyperbolic, Together AI
  • Corporate Sponsors — XTX Markets, Google.org
  • Funding & Philanthropy — AI for Math Fund, NSF, DARPA
• Quick Links
• Timeline: Key Milestones

Resources

• Tools & Platforms
• Learning Resources
  • YouTube Channels
  • Seminars
  • Podcasts
  • Courses
  • Blogs & Newsletters
• Research & Papers
  • Preprint Platforms
  • Landmark Papers
• Communities
• People

---

Proof Assistants

Dependent Type / HoTT

Lean

Microsoft Research → Lean FRO. Created by Leonardo de Moura.

Core

• Lean 4 - Functional programming language and theorem prover
• Mathlib - The math library for Lean 4, largest unified formalized math library
• Lake - Lean's build system and package manager
• Batteries - Extended standard library for Lean 4 (formerly std4)

Learning

• Mathematics in Lean - Interactive tutorial for mathematical formalization
• Theorem Proving in Lean 4 - Official introduction to theorem proving
• Functional Programming in Lean - Learn Lean as a programming language
• Natural Number Game - Gamified introduction to Lean proofs
• The Mechanics of Proof - Undergraduate introduction to proofs using Lean

Tools

• Lean 4 VS Code Extension - Official VS Code integration
• Blueprint - Generate dependency graphs for Lean projects
• doc-gen4 - Documentation generator for Lean 4
• Paperproof - Visual proof interface for Lean
• LeanInfer - Run neural network inference in Lean
• Pantograph - Machine-to-machine interaction for Lean

Projects

• FLT - Fermat's Last Theorem formalization (in progress)
• PFR - Polynomial Freiman-Ruzsa conjecture formalization
• Sphere Eversion - Formalized proof of sphere eversion
• Liquid Tensor Experiment - Scholze's liquid tensor experiment
• Prime Number Theorem - Prime Number Theorem and more

Coq / Rocq

INRIA. Renamed to Rocq in 2024.

• Rocq (Coq) - The Coq proof assistant, now renamed to Rocq
• MathComp - Mathematical Components library
• Software Foundations - Classic introduction to Coq
• Certified Programming with Dependent Types - Advanced Coq programming

Agda

Chalmers University, Sweden.

• Agda - Dependently typed programming language and proof assistant
• agda-stdlib - Agda standard library
• Cubical Agda - Cubical type theory mode in Agda
• Programming Language Foundations in Agda - Textbook on PL theory in Agda

Idris

Created by Edwin Brady.

• Idris 2 - Dependently typed language with quantitative types
• Idris 1 - Original Idris implementation
• Type-Driven Development with Idris - Official book by Edwin Brady

F*

Microsoft Research. SMT-driven verification.

• F* - Verification-oriented ML dialect with dependent types
• Everest - Verified secure implementations using F*

Arend

JetBrains. Native HoTT support.

• Arend - Theorem prover with native homotopy type theory
• Arend Lib - Standard library with HoTT foundations

Aya

Chinese team. Based on cubical type theory.

• Aya - Cubical type theory based proof assistant

HOL Family

Isabelle

Cambridge & TU München.

• Isabelle - Generic proof assistant, primarily used with HOL
• Archive of Formal Proofs - Large collection of proof libraries for Isabelle

HOL4

Primary successor to the HOL system.

• HOL4 - Interactive theorem prover for higher-order logic

HOL Light

Created by John Harrison. Minimalist design.

• HOL Light - Simplified HOL prover, used in Flyspeck project

ProofPower

Industrial-grade HOL system.

• ProofPower - Tool suite for specification and proof in HOL and Z

IMPS

• IMPS - Interactive Mathematical Proof System

Other Important Systems

Mizar

Tarski-Grothendieck set theory. One of the largest formalized math libraries.

• Mizar - System for formalizing mathematics
• Mizar Mathematical Library - Extensive library of formalized mathematics

Metamath

Minimalist approach to formal verification.

• Metamath - Tiny language for developing formal math databases
• set.mm - Main Metamath database for set theory

PVS

SRI International.

• PVS - Prototype Verification System

ACL2

Boyer-Moore tradition.

• ACL2 - Computational Logic for Applicative Common Lisp

Nuprl

Cornell University. Extended type theory.

• Nuprl - Proof development system based on constructive type theory

Dafny

Microsoft. Program verification.

• Dafny - Verification-aware programming language

Atelier B

B method for industrial applications.

• Atelier B - Industrial tool for B method formal development

Cubical Type Theory

• cubicaltt - Experimental implementation of cubical type theory
• redtt - Experimental proof assistant for cartesian cubical type theory
• cooltt - Cool elaborator for cartesian cubical type theory (successor to redtt)
• RedPRL - Proof assistant for computational cubical type theory
• yacctt - Yet another cubical type theory

Logical Frameworks

• Twelf - Implementation of the LF logical framework
• Dedukti - Universal proof checker based on λΠ-calculus modulo
• Beluga - Proof environment for contextual modal types (McGill)
• Abella - Interactive theorem prover based on λ-tree syntax

Historical Systems

Pioneering systems that shaped the field.

• Automath - First proof checker (1967, de Bruijn)
• LCF - Logic for Computable Functions (origin of ML language)
• Nqthm - Boyer-Moore theorem prover (predecessor to ACL2)
• LEGO - Edinburgh proof assistant
• Matita - Coq-like system (no longer maintained)
• MINLOG - System for first-order minimal logic
• ALF - Another Logical Framework

Other / Emerging

• Acorn - AI-integrated theorem prover by Kevin Lacker
• Andromeda - Type theory with equality reflection
• litex - Simple formal language learnable in 2 hours (Website)
• Liquid Haskell - Refinement types for Haskell
• Rzk - Proof assistant for simplicial type theory

---

AI for Formal Mathematics

The 2024-2025 explosion of AI tools for theorem proving

Neural Theorem Provers

Fully automated systems that generate formal proofs

IMO-Level Systems (2025)

Open Source Provers

• Goedel-Prover - Princeton, SOTA open-source, scaffolded data synthesis
• Goedel-Prover-V2 - 90.4% MiniF2F, self-correction mode
• DeepSeek-Prover-V2 - 671B model, subgoal decomposition
• Kimina-Prover - 72B, formal reasoning pattern, distilled 1.5B/7B
• BFS-Prover - ByteDance, scalable best-first tree search
• Morph Prover v0 7B - Morph Labs, open-source conversational prover

Commercial/Closed Systems

• Aristotle - Harmonic AI, IMO Gold, API available
• Seed-Prover - ByteDance, Seed-Geometry for geometry
• AlphaProof - DeepMind, Nature 2025
• Gauss - Math Inc., autoformalization agent, Strong PNT in 3 weeks

Research Papers

• AlphaProof Paper - Nature, Nov 2025
• A Survey on Deep Learning for Theorem Proving - Comprehensive paper list
• Formal Mathematical Reasoning: A New Frontier in AI - Position paper

IDE & Copilot Tools

Human-AI collaborative tools for proof development

VS Code Extensions

• Mozi Lean Copilot - PKU AI4Math + IQuest, generate→verify→feedback loop, LeanSearch integration (Beta)
• Lean Copilot - Caltech/LeanDojo, suggest_tactics, search_proof, premise selection
• llmstep - Lightweight tactic suggestions, model-agnostic
• LLMLean - OpenAI/local LLM integration

Cloud IDEs

• ReasLab IDE - PKU BICMR, zero-install browser IDE, real-time collaboration
• Lean 4 Web - Official Lean playground

Commercial APIs

• Aristotle API - Harmonic, fill sorry, counterexamples, Mathlib integration

Search Engines

Finding theorems and lemmas in formal libraries

• LeanSearch - PKU BICMR (ReasLab), natural language semantic search for Mathlib4
• Loogle - Lean FRO, type signature search (like Hoogle for Haskell)
• LeanExplore - Multi-library search, MCP server support
• Moogle - Early semantic search engine

Infrastructure & Frameworks

Tools for building AI theorem provers

Data Extraction & Interaction

• LeanDojo - Caltech, Python interaction, data extraction, ReProver
• LeanDojo-v2 - End-to-end framework for Lean 4
• Jixia (稷下) - PKU BICMR, static analysis, ML data extraction
• Pantograph - Lean 4 interaction library

High-Performance Servers

• Kimina Lean Server - Moonshot AI, high-performance REPL for RL training
• Jixia-interactive - PKU, REAL-Prover environment

Agent Frameworks

• LeanAgent - Caltech, lifelong learning, auto PR generation
• lean-agentic - MCP server, vector memory, Claude Code integration
• P2PCLAW - Decentralized peer-reviewed science network combining P2P collaboration, Lean 4 formal verification, AI agents, and community-driven scientific publishing

Retrieval & Premise Selection

• REAL-Prover - PKU, retrieval-augmented Lean prover
• LeanSearch-PS - Semantic premise selection

Benchmarks & Datasets

Evaluating AI theorem provers

Competition Math

Advanced Mathematics

• NuminaMath-LEAN - 104K competition problems formalized

General Benchmarks

• Lean Workbook - Large-scale problem set
• miniCTX - In-context theorem proving
• TPTP - Thousands of Problems for Theorem Provers

Autoformalization

Translating natural language to formal proofs

• Kimina-Autoformalizer - Numina/Moonshot, 80% MiniF2F pass rate
• Herald - Natural language annotated Lean 4 dataset
• FormalAlign - Alignment evaluation for autoformalization
• Draft-Sketch-Prove - Informal to formal pipeline

Geometry Solvers

Specialized systems for Euclidean geometry

• AlphaGeometry 2 - DeepMind, IMO geometry
• Seed-Geometry - ByteDance, instant geometry verification
• Yuclid/Newclid - Harmonic AI, open-sourced geometry solver
• LeanGeo - Numina + PKU, geometry in Lean 4

Agentic CLI Tools

General-purpose AI coding assistants that work with Lean

• Claude Code - Anthropic, MCP support, agentic terminal
• OpenAI Codex CLI - OpenAI, GPT-5 powered
• Aider - Open source, multi-model support
• Cline - VS Code + CLI, autonomous agent

---

Automated Theorem Provers (Classical)

Traditional symbolic reasoning systems

First-Order ATPs

• Vampire - Most successful ATP, CASC winner
• E Prover - Efficient equational reasoning
• SPASS - Automated theorem prover
• Prover9 - Resolution/paramodulation

SMT Solvers

• Z3 - Microsoft, most popular SMT solver
• CVC5 - Stanford, SMT-COMP winner
• Yices - SRI, efficient SMT solver

Integration with Proof Assistants

• Sledgehammer - Isabelle + external ATPs
• Lean-SMT - Lean 4 + SMT solvers (cvc5)
• Duper - Superposition prover for Lean 4

---

Companies & Organizations

AI Math Startups

Company Details

Harmonic AI (Palo Alto)

• Founders: Vlad Tenev (Robinhood CEO), Tudor Achim
• Investors: Sequoia, Kleiner Perkins, Index Ventures, Ribbit Capital
• Achievements: IMO 2025 Gold (5/6), 98%+ MiniF2F, Erdős Problem #124
• Focus: Mathematical Superintelligence (MSI), hallucination-free AI

Axiom Math (San Francisco)

• Founder: Carina Hong (Stanford dropout, MIT/Oxford background)
• CTO: Shubho Sengupta (ex-Meta FAIR)
• Team: François Charton, Aram Markosyan, Hugh Leather (ex-Meta FAIR)
• Investors: B Capital (lead), Greycroft, Madrona, Menlo Ventures
• Focus: Auto-formalizer, Conjecturer, Prover, Knowledge Base

Math Inc.

• Founder: Christian Szegedy (ex-xAI, ex-Google, inventor of Batch Norm & adversarial examples)
• Achievements: Strong Prime Number Theorem formalization in 3 weeks (vs 18+ months human effort)
• Focus: Autoformalization at scale, verified superintelligence

Morph Labs (San Francisco)

• Founder: Jesse Han
• Products: Morph Prover v0 7B, Trinity autoformalization system, Infinibranch
• Focus: Cloud for superintelligence, AI-human collaboration

Research Organizations

Organization Details

Lean FRO (Focused Research Organization)

• Founded: July 2023 (within Convergent Research)
• Leadership: Leonardo de Moura (Chief Architect, Lean creator), Sebastian Ullrich (Head of Engineering)
• Funders: Simons Foundation, Alfred P. Sloan Foundation, Richard Merkin Foundation, Alex Gerko ($10M, July 2025)
• Focus: Lean scalability, usability, proof automation, documentation

Project Numina

• Founded: Late 2023
• Founders: Jia Li, Yann Fleureau, Guillaume Lample, Stan Polu, Hélène Evain
• Partners: Hugging Face, Mistral AI, General Catalyst, Answer.AI, PKU BICMR
• Achievements: Won AIMO 2024 Progress Prize
• Products: NuminaMath, Kimina-Autoformalizer, LeanGeo

Academic Labs

Big Tech AI Labs

Lab Details

Google DeepMind

• AI for Math Initiative: Funding + technology support
• Partners: Imperial College, IAS, IHES, Simons Institute, TIFR
• Technology: Provides Gemini Deep Think, AlphaEvolve, AlphaProof to collaborators

AWS Automated Reasoning Group

• Key person: Leonardo de Moura (Lean creator, Senior Principal Applied Scientist)
• Cedar - Authorization policy language with Lean verification
• Amazon Bedrock Automated Reasoning checks (2025) - Formal verification to reduce AI hallucinations

Compute Infrastructure

GPU and compute providers for AI4Math research

Hyperbolic

Most AI4Math-relevant compute provider

• Founders: Jasper Zhang PhD (UC Berkeley Math), Yuchen Jin PhD
• Funding: $7M Seed (Polychain + Lightspeed), $12M Series (Variant)
• Users: 195,000+ developers including Stanford, Berkeley, Hugging Face, LMSYS
• Technology: Hyper-dOS, Proof of Sampling (PoSP)

Corporate Sponsors

Funding & Philanthropy

A guide to AI4Math funding opportunities for researchers, startups, and builders

Overview

AI for Math Fund (XTX Markets + Renaissance Philanthropy)

Most relevant AI4Math-specific funding

• Total: $18M (first round, doubled from initial $9.2M)
• Per grant: Up to $1,000,000
• Duration: Up to 24 months
• Eligibility: Researchers, nonprofits, companies, mathematicians, software engineers
• Advisor: Terence Tao (Fields Medalist)
• Website: renaissancephilanthropy.org
• 2025 Recipients: 29 inaugural grants

Focus Areas:

1. Production-ready open-source tools (autoformalization, proof generation, verified code synthesis)
2. Open datasets of theorems, proofs, math problems
3. Field building (textbooks, courses, community resources)
4. Moonshot ideas (high-risk, high-reward AI math research)

NSF AIMing Program

Primary US government AI+Math funding

• Program: NSF 24-554
• Amount: $500,000 - $1,200,000 per grant
• Duration: Up to 3 years
• Annual budget: ~$6M (6-10 projects/year)
• Eligibility: US academic institutions
• Website: nsf.gov/funding/opportunities/aiming

DARPA expMath (Exponentiating Mathematics)

DARPA frontier research program

• Goal: Develop AI collaborators to accelerate pure mathematics by orders of magnitude
• Duration: 36 months
• Program Manager: Patrick Shafto
• Website: darpa.mil/research/programs/expmath
• Note: Contracts only (no grants), focuses on pure mathematics

NSF SBIR/STTR

Non-dilutive funding for US startups

• Phase I: $50,000 - $500,000 (6-12 months)
• Phase II: Up to $2,000,000
• Success rate: Phase I ~20%, Phase II 40-60%
• Eligibility: US small business (51%+ US citizen/PR ownership)
• Website: seedfund.nsf.gov

Other Programs

Simons Foundation

• Major funder of Lean FRO (with Sloan Foundation, Merkin Foundation)
• Simons Collaborations in MPS, Targeted Grants
• simonsfoundation.org

NSF ICARM (Institute for Computer-Assisted Reasoning in Mathematics)

• Host: Carnegie Mellon University
• Funded by: NSF + Simons Foundation
• Focus: Formal methods, AI, ML for mathematical research

AIMO Prize (AI Math Olympiad)

• Sponsor: XTX Markets / Alex Gerko
• Goal: AI that achieves IMO gold medal
• Progress Prize 2024: Won by Project Numina

Accelerators & Corporate Programs

Application Strategy

For Startups:

1. AI for Math Fund - accepts companies, up to $1M non-dilutive
2. NSF SBIR/STTR - requires US entity, quick seed funding
3. Stack accelerators: YC + Google AI First + NVIDIA Inception

For Academics:

1. NSF AIMing - primary funding source
2. AI for Math Fund - open-source tools and datasets
3. Simons Foundation - long-term collaborations

---

Quick Links

• 📊 AI4Math Leaderboard - Papers with Code
• 📚 DL4TP Survey - Deep Learning for Theorem Proving
• 🎓 Formal Mathematical Reasoning - Position paper on AI4Math
• 🏆 IMO Grand Challenge - AI for IMO problems

Funding:

• 💰 AI for Math Fund - Up to $1M grants
• 🇺🇸 NSF AIMing - $500K-$1.2M
• 🛡️ DARPA expMath - Frontier research
• 🚀 NSF SBIR/STTR - Startup funding

---

Timeline: Key Milestones

---

Tools & Platforms

Learning Resources

YouTube Channels

Mathematicians

• Terence Tao - Fields Medalist on math and AI

Math Education

• 3Blue1Brown - Beautiful math visualizations by Grant Sanderson
• Numberphile - Popular math content
• Mathologer - Mathematical explanations
• Stand-up Maths - Matt Parker's math entertainment

Academic Lectures

• Oxford Mathematics - Oxford undergraduate lectures and public talks
• Institute for Advanced Study - IAS talks
• Fields Institute - Mathematics conferences
• Simons Institute - Theory of Computing lectures

Seminars

• Every Proof Assistant - Survey of proof assistants, hosted by Andrej Bauer (Vimeo)
• HOTTEST - HoTT Electronic Seminar Talks
• Lean On Me - Lean online learning seminar organized by Ben Chow (UCSD) and Zilu Ma (UT Knoxville)

Podcasts

• Lex Fridman Podcast - Interviews with mathematicians like Terence Tao
• The Joy of Why - Steven Strogatz on Quanta Magazine

Courses

Blogs & Newsletters

• Xena Project - Kevin Buzzard's blog on formalization
• Lean Community Blog - Updates from the Lean community
• Quanta Magazine - Quality math journalism

Research & Papers

Preprint Platforms

• aiXiv - Next-generation preprint server for AI scientists with multi-agent review system (GitHub)
• arXiv - Open-access preprint repository for scientific papers

Landmark Papers

Communities

• Lean Zulip - Official Lean community chat
• Lean Discord - Lean community Discord server
• Rocq Zulip - Rocq (formerly Coq) community chat
• Machine Learning for Theorem Proving - Research community

People

---

Contributing

Contributions welcome! Please read the contributing guidelines first.

License

MIT

---

_{Curated with care by the community}