# Towards Evolutionary Theorem Proving for Isabelle/HOL

arXiv: https://arxiv.org/abs/1904.08468 · HTML: https://mlsanity.com/paper/1904.08468/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Apr 2019.

## Built on by (most cited first, 4 of 4)

- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Genetic Algorithm for Program Synthesis](https://mlsanity.com/paper/2211.11937/) (2022)
- [EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages](https://mlsanity.com/paper/2402.16878/) (2024)
- [ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving](https://mlsanity.com/paper/2608.26334/) (2026)

## Abstract (arXiv)

Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers' expertise and remains labor intensive. Recently, researchers have extracted heuristics of interactive proof development from existing large proof corpora using supervised learning. However, such existing proof corpora present only one way of proving conjectures, while there are often multiple equivalently effective ways to prove one conjecture. In this abstract, we identify challenges in discovering heuristics for automatic proof search and propose our novel approach to improve heuristics of automatic proof search in Isabelle/HOL using evolutionary computation.