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.

A Minimal Agent for Automated Theorem Proving

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

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.

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

Automated theorem prover for Multiplicative Linear Logic

Multi-agent math prover — Claude agents propose, Lean 4 disposes

Plan, generate, and kernel-check Lean 4 proofs in sandboxes.

Self-hostable paraconsistent HoTT LLM-to-Lean acceptance gateway. Runs proof attempts through security preflight, Lean checks, theorem-fingerprint locks, and ShadowHoTT bilattice routing for accept/repair/reject/human-review decisions.

NAMM: verification-first research on machine-native math discovery. Math structures as observer-independent objects; human formalism as bounded coordinates. Falsifiable SNH gates, K_A/K_H asymmetry, experiments 001-006. Updates: https://x.com/agiminister · https://anthemium.tech

Autonomous Equational Theorem Discovery Engine & Mathematical Observatory with E-Graphs, Knuth-Bendix Completion, and Microsecond Finite Countermodels

Autonomous automated theorem prover combining language-model proof search with Lean 4 verification.

Can a machine recover mathematical structure from an anonymized formal theory and a proof checker alone?