An AI-powered conjecture exploration engine. Generates candidate mathematical hypotheses via LLM, auto-formalizes them in Lean 4, and logs every experiment in a reproducible, snapshot-based research environment. Built on ProofX infrastructure.
reproducible-research theorem-proving computational-mathematics formal-verification lean4 proofx ai-for-math conjecture-generation
-
Updated
Apr 25, 2026 - Python