automated-theorem-proving

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

course project for hands-on data science (DATA 1030) at brown university

A tool for automatically verifying whether a given first-order logic formula is a tautology, based on Herbrand's theory and the Davis-Putnam SAT solver. Implemented in C++.

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

An automated theorem prover for a subset of first order logic written in Rust

ParadigmForge: a governed architecture for machine-generated mathematical theory formation (design-and-protocol paper). Extends the Bourbaki Engine from claim promotion to governed theory formation.

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

English reasoning test cases with expected answers, plus recorded multi-LLM results and analysis for the nlpsolver natural-language-to-logic parser and gk theorem prover.

Executable mathematics: typed structures, verifiable morphisms, proofs, figures, and replayable certificates.

Verified prove-or-disprove harness for algebraic conjectures

Brokers proof goals from Lean 4 and Rocq through a shared IR to SMT solvers, ATPs, and LLM provers, then verifies returned certificates and lifts proof terms back to the home system.

A from-scratch TypeScript DDAR geometry proof-checker (deductive database + algebraic reasoning, the symbolic method behind AlphaGeometry) that verifies olympiad proof steps against several resampled figures, plus the interactive geometry course built on it.

automated design and discovery in any field that can be represented by logic

Mapping the hidden geometry between Lean theorem statements, proof strategies, and retrieval-guided proof generation.

Two-week certificate-first campaign: an LLM orchestrating ATPs, SAT, and GAP against open problems in quasigroup, loop, and semigroup theory — closed two open orders of a 1998 conjecture; the trust protocol is the point

Weighted Erdős–Szekeres (Erdős #1026) in Lean 4 / Mathlib — human-scale proof plus a referee report, failure atlas, and extracted benchmarks for AI theorem-proving

a formally verified, automated prover for the first-order logic

TPTP ensemble/portfolio theorem prover runner and benchmark harness

Magma signature and coverage engine over the Equational Theories Project law set