Tool for data extraction and interacting with Lean programmatically.

Retrieval-Augmented Theorem Provers for Lean

llmstep: [L]LM proofstep suggestions in Lean 4.

A Low Barrier Proof Assistant

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

ChatGPT plugin for theorem proving in Lean

Resolution theorem proving for predicate logic in pure Python.

Jupyter kernel for Coq

A template for blueprint-driven formalization projects in Lean.

LeanInteract: A Python Interface for Lean 4

An environment for learning formal mathematical reasoning from scratch

Tiny theorem prover with syntax like Lean 4 in <1K LOC

Solving Inequality Proofs with Large Language Models.

Python Symbolic Information Theoretic Inequality Prover

Implementation and subsequent optimization for "Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models"

Autonomous Theorem Prover for First Order Predicate Logic

multi-logic proof generator

Four color theorem, Guthrie, Kempe, Tait and other people and stuff

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

a constraint-based syntax-guided synthesis (SyGuS) engine