OpenClaw-style theorem proving

Lean 4 programming language and theorem prover

Anonymous HF dataset for double blind review sharing

How good are LLMs at generating Lean code

Universal math embedder

Lean 4 theorem proving skill and workflow pack for AI coding agents

An MCP server that allows AI assistants to connect with Google Gemini's command-line interface, taking advantage of Gemini's large token capacity to analyze large files and understand codebases.

MCP server wrapper for OpenAI Codex CLI that enables Claude Code to leverage Codex's AI capabilities directly.

UlamAI is an open-source Lean theorem prover and formalizer.

Formalizing the Category of Poly in Lean

The best ChatGPT that $100 can buy.

Lean Theorem Prover MCP

Solve the Vlasov-Landau equations using SBTM

Code to verify citations in a bibtex file

Academia MCP server: Tools for automatic scientific research

PDE Lean formalization

Eric'sW26 Course on Lean

Semantic Search Over 9 million Mathematical Theorems

Formalizing the basic definitions and results of polyhedral geometry in Lean 4.