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

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

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

A Minimal Agent for Automated Theorem Proving

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 prototype framework for automated theory construction in Lean 4.

Brute force math problem solving

🪶 Neural premise selection for Agda.

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

mai: MAth Interpreter with Standard Foundations

HOL-Light Library for Modal Systems

A reasoner for Input/Output logic

LLMs + Lean, on your laptop or in the cloud

Example axiom and problem files within the TPTP Format

Elaboración de demostraciones con Lean.

HOL Light Library for Modal Systems

A simple repackaging of the Vampire automated theorem prover