Resources

Companies — Research Labs

• AI-MO (AI Mathematical Olympiad) Global

  Initiative to create AI systems capable of achieving gold medal performance at the International ...

• Anthropic San Francisco, USA

  AI safety company developing Claude. Claude demonstrates strong mathematical reasoning capabiliti...

• Cohere Toronto, Canada / London, UK

• Compfiles Open Source

  Catalog of Math Problems Formalized in Lean. A collection of competition math problems and other ...

• Google DeepMind London, UK

  AI research lab with significant work in mathematical reasoning. Creator of AlphaGeometry and Alp...

• Math Inc. USA

  AI incubator and research lab focused on mathematical intelligence. Building and investing in com...

• Mistral AI Paris, France

  French AI company developing open-weight language models with strong mathematical reasoning capab...

• OpenAI (Math/Reasoning Team) San Francisco, USA

  Research lab developing GPT models with mathematical reasoning capabilities. Creator of GPT-f and...

• PRISM AI USA

  AI-powered platform for mathematical research assistance. Provides theorem discovery, proof sugge...

• ResLab (Research Laboratory) China

  Cross-disciplinary research lab focusing on AI for mathematics, formal verification, and automate...

Companies — AI Math Education

• AutoDiscovery (Allen Institute for AI) Seattle, USA

  AI-powered research discovery platform from Allen Institute for AI. Helps researchers discover co...

• Elicit USA

  AI research assistant that helps researchers find and synthesize academic papers. Strong capabili...

• Frenzy Math Beijing, China (Peking University)

  AI-powered math education platform focused on Olympiad-level problem solving. Uses advanced LLMs ...

• PKU Formal Mathematics Course Beijing, China (Peking University)

  北京大学形式化数学课程资料 - Course materials on formal mathematics and Lean 4 from Peking University (BICMR)....

• ReasLab Alpha China

  Interactive platform for AI-powered mathematical reasoning and proof exploration. ReasLab Alpha p...

Companies — Theorem Proving

• Harmonic AI USA

  Building AI systems for mathematical reasoning and theorem proving. Focus on combining deep learn...

• Maritza AI USA

  Building AI systems for mathematical discovery and formal verification. Focus on automated theore...

• Project Numina Global (Open Source)

  Open-source AI4Math research project creating datasets, models, and benchmarks for mathematical r...

Companies — Math Engines & Tools

• Maplesoft Math Reasoning Engines · Waterloo, Ontario, Canada

  Creators of Maple, a leading symbolic and numeric computing environment. Focus on mathematics edu...

• SageMath Symbolic Computation · Open Source

  Free open-source mathematics software system. Combines the power of many existing open-source pac...

• Symbolica AI Math Reasoning Engines · USA

  Building AI systems for symbolic mathematics and computer algebra. Focus on making symbolic compu...

• Wolfram Research Math Reasoning Engines · Champaign, Illinois, USA

  Creators of Mathematica and Wolfram Alpha. Pioneers in symbolic computation and computational kno...

Companies — Formal Verification

• lean4lean Global

  A project to formally verify Lean 4 itself using Lean 4. Creating a verified typechecker and kern...

• TheoremOne USA

  Automated theorem proving for software verification. Industrial-grade formal verification tools u...

---

Open Source Projects

• Agda ⭐ 2.2k

• Astral ⭐ 250

  AI-powered proof assistant for Lean 4. Provides intelligent tactic suggestions and automated proo...

• CoqHammer ⭐ 400

  Automated reasoning tool for Coq that combines machine learning with automated theorem provers. P...

• Dafny ⭐ 4.5k

• dsp-theorem-proving ⭐ 300

  Demonstration-Search Planning for theorem proving. Combines language models with search algorithm...

• GeoCoq ⭐ 300

  Formalization of geometry in Coq based on Tarski's axioms. Comprehensive treatment of Euclidean a...

• HOL4 ⭐ 350

  Interactive theorem prover for higher-order logic. The system of choice for verification of ARM p...

• HOList ⭐ 500

  Google Research's environment for neural theorem proving in Higher-Order Logic (HOL Light). Used ...

• Isabelle/HOL ⭐ 900

  A generic proof assistant for higher-order logic. One of the most widely used theorem provers for...

• Lean 4: A Programmer-oriented Theorem Prover ⭐ 3.5k

  A new version of Lean with improved performance and metaprogramming capabilities. Used for both f...

• LLMLean

  Integrates LLMs with Lean for tactic suggestions, proof completion, and more. Supports OpenAI, To...

• Math Paper Analyzer

  Automatic extraction of mathematical structures (definitions, theorems, lemmas, etc.) from papers...

• mathlib4 ⭐ 2.1k

  The unified library of mathematics for Lean 4. Contains formalized mathematics spanning algebraic...

• Metamath ⭐ 600

  A tiny language that can express theorems in abstract mathematics, accompanied by proofs that can...

• miniF2F-lean4 ⭐ 50

  miniF2F dataset ported into Lean 4. Contains formalized competition mathematics problems from AMC...

• MiniF2F ⭐ 400

  Benchmark for automated theorem proving on high-school competition problems. Contains problems fr...

• ProofNet ⭐ 150

  Benchmark for autoformalization and theorem proving in mathematics. Contains parallel corpus of i...

• ProveAgent ⭐ 10

  An agent for automated theorem proving. Experimental project exploring agent-based approaches to ...

• PVS ⭐ 200

  Prototype Verification System - specification language integrated with support tools and theorem ...

• Sledgehammer ⭐ Built-in

  Automated theorem prover for Isabelle/HOL. Translates proof goals to external ATPs (E, SPASS, Vam...

• Tactician ⭐ 150

  AI-powered tactic suggestion system for Coq. Uses machine learning to predict the next tactic in ...

• Z3 Theorem Prover ⭐ 10k

  An efficient SMT solver from Microsoft Research. Widely used in software verification, test gener...

Tools

• Coq Formal Proof

  Classic interactive theorem prover widely used in formal mathematics and program verification

• Lean 4 Formal Proof

  Next-generation theorem prover and programming language with dependent types and the powerful mat...

• Mathematica / Wolfram Language Symbolic Computation

  Powerful symbolic computation system covering all areas of mathematics, science, and engineering