FunSearch
A program-evolution framework that searches for mathematical constructions using executable scoring functions. - Developer / Organization: G…
AI & Academia
Axplorer
An open tool that learns from promising examples to search for extremal mathematical constructions. - Developer / Organization: Axiom Math -…
AxProverBase
A minimal Lean proving agent built around iterative proposals, compilation, review and memory. - Developer / Organization: Axiomatic AI; Bor…
Goedel-Architect
A formal proving framework that generates, proves and refines dependency graphs of lemmas. - Developer / Organization: Jui-Hui Chung and col…
Prover Agent
A theorem-proving agent that combines informal reasoning with formal Lean feedback. - Developer / Organization: Kaito Baba, Chaoran Liu, Shu…
LeanMarathon
A multi-agent harness for carrying long mathematical proofs through Lean formalization. - Developer / Organization: Yuanhe Zhang, Yuekai Sun…
Numina-Lean-Agent
A mathematical agent combining a coding assistant with Lean feedback, theorem search and reasoning tools. - Developer / Organization: Projec…
OpenGauss
An open Lean workflow orchestrator for AI-assisted proving, formalization and proof review. - Developer / Organization: Math, Inc. and open-…
QED (proofQED)
A multi-agent system that plans, writes and reviews natural-language proofs for research problems. - Developer / Organization: Chenyang An,…
Pharos (FrenzyMath)
A research orchestration system that coordinates mathematical approaches, workers and model-based review. - Developer / Organization: Bin Do…
Danus (FrenzyMath)
A multi-agent mathematics system that organizes proof attempts around a shared graph of claims. - Developer / Organization: FrenzyMath / Dan…
Rethlas-OSV
A desktop workflow combining Rethlas proof generation with OSVerify review. - Developer / Organization: OSVerify and Rethlas teams; desktop…
37–48 of 50 discussions