Learning-assisted theorem proving with millions of lemmas

Area of Science:

• Formal mathematics
• Automated theorem proving
• Mathematical knowledge management

Background:

• Formal mathematical libraries contain millions of inference steps and proved statements (lemmas).
• A small fraction of these lemmas are named and reused in subsequent proofs.
• Current methods lack efficient ways to identify and leverage the most useful lemmas.

Purpose of the Study:

• To develop and implement criteria for estimating the usefulness of lemmas in formal libraries.
• To mine large inference graphs for high-utility lemmas.
• To improve automated theorem proving by enhancing lemma reusability.

Main Methods:

• Defined criteria for estimating lemma usefulness within the HOL Light system.
• Mined the inference graphs of HOL Light and Flyspeck libraries.
• Integrated learning-based relevance filtering with the identified useful lemmas.

Main Results:

• Successfully identified and curated millions of high-utility lemmas.
• Demonstrated significant strengthening of automated theorem proving for new conjectures.
• Showcased the effectiveness of combining lemma usefulness criteria with relevance filtering.

Conclusions:

• The proposed criteria effectively identify reusable lemmas in large formal libraries.
• Enhanced lemma reusability significantly boosts automated theorem proving capabilities.
• This approach offers a scalable solution for managing and utilizing formal mathematical knowledge.