Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques

The challenge of formal proof generation has a rich history, but with modern techniques, we may finally be at the stage of making actual progress in real-life mathematical problems. This paper explores the integration of ChatGPT and basic searching techniques to simplify generating formal proofs, with a particular focus on the miniF2F dataset. We demonstrate how combining a large language model like ChatGPT with a formal language such as Lean, which has the added advantage of being verifiable, enhances the efficiency and accessibility of formal proof generation. Despite its simplicity, our best-performing Lean-based model surpasses all known benchmarks with a 31.15% pass rate. We extend our experiments to include other datasets and employ alternative language models, showcasing our models' comparable performance in diverse settings and allowing for a more nuanced analysis of our results. Our findings offer insights into AI-assisted formal proof generation, suggesting a promising direction for future research in formal mathematical proof.

@article{han2025_2502.03321,
  title={ Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques },
  author={ Sangjun Han and Taeil Hur and Youngmi Hur and Kathy Sangkyung Lee and Myungyoon Lee and Hyojae Lim },
  journal={arXiv preprint arXiv:2502.03321},
  year={ 2025 }
}