ProofCraft

ProofCraft is a sophisticated tool that bridges the gap between Large Language Models and formal mathematics verification using Lean 4.

Key Features

• Multi-agent orchestration for proof search
• LLM response caching with 70-90% cost reduction
• Support for multiple search strategies (DFS, BFS, Best-First)
• Interactive web UI built with Gradio
• Achieved 28.3% success rate on miniF2F benchmark

Research Impact

This project demonstrates how modern LLMs can assist in formal mathematics, making theorem proving more accessible and efficient. The caching system significantly reduces API costs while maintaining proof quality.