automated-theorem-proving

A Machine-to-Machine Interaction System for Lean 4.

A universal, atomic library of mathematics and tools for agents to compose them.

GCLC is a mathematical software tool for producing high-quality mathematical illustrations, for teaching mathematics, and for automated proving of geometry theorems.

A Minimal Agent for Automated Theorem Proving

Code & data for ICLR 2024 spotlight paper: 🍯MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data

A multi-agent AI framework formalizing the Yang-Mills Mass Gap finite-lattice theory in Lean 4 without axioms or sorry.

OpenATP is an open-source Python package providing a common interface for Automated Theorem Proving (ATP)

Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

MathTensor Lean 4 formalizations of Putnam 2025 problems, with machine-verified Mathlib proofs.

Rust interface for cvc5

A Lean 4 library of machine-generated, kernel-verified mathematics.

A prototype framework for automated theory construction in Lean 4.

Brute force math problem solving

🪶 Neural premise selection for Agda.

mai: MAth Interpreter with Standard Foundations

Official implementation of "FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving"

StarExec-ARC is a framework for containerizing Automated Theorem Proving (ATP) systems. It simplifies the deployment and scaling of ATPs using Podman and Kubernetes, enabling researchers to easily benchmark solvers in a modern, containerized StarExec environment.

A tool for parsing and visualizing ontology files written in the Ontol DSL

HOL-Light Library for Modal Systems

Mathematics Distillation Challenge, Equational Theories. Stage 1 cheatsheet and Stage 2 Lean 4 certificate solver for the SAIR Foundation competition.