Source-linked AI summary
Learning-Assisted Automated Reasoning with Flyspeck
Cezary Kaliszyk, Josef Urban
TL;DR
The paper asks whether Flyspeck’s formal mathematical library can support broad automated theorem proving in HOL Light, where a general large-theory ATP/AI bridge was missing. It combines sound logic translations, exported dependencies, learned premise selection, and external ATPs, then evaluates them in chronological re-proving experiments. In push-button mode, 39% of theorems were proved within 30 seconds on a 14-CPU workstation, while proof-dependent and combined methods reached 50% and 56%.
Problem
HOL Light lacked a general large-theory ATP/AI bridge capable of selecting relevant library knowledge and running external provers for new goals.
Method
The paper combines sound HOL Light translations, exported theorem dependencies, learned formula representations, premise selectors, and external ATPs integrated as HOL Light advisors.
Results
39% of Flyspeck theorems were proved within 30 seconds in fully automated push-button mode, while proof-dependent methods reached 50% and all evaluated methods reached 56%.
Takeaways & Limitations
Learning-advised ATPs can sometimes produce substantially different or simpler proofs and discover duplications in the formal library.
Takeaways & Limitations
The system does not yet learn the precise or fuzzy high-level pathfinding characteristic of human proofs, and advised proofs can be more complicated than original proofs.
Abstract
from arXiv · showhide
The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the proofs, producing an AI system capable of answering a wide range of mathematical queries automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of Flyspeck from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39% of the 14185 theorems could be proved in a push-button mode (without any high-level advice and user interaction) in 30 seconds of real time on a fourteen-CPU workstation. The necessary work involves: (i) an implementation of sound translations of the HOL Light logic to ATP formalisms: untyped first-order, polymorphic typed first-order, and typed higher-order, (ii) export of the dependency information from HOL Light and ATP proofs for the machine learners, and (iii) choice of suitable representations and methods for learning from previous proofs, and their integration as advisors with HOL Light. This work is described and discussed here, and an initial analysis of the body of proofs that were found fully automatically is provided.
1 Introduction and Motivation
The paper addresses the lack of a general large-theory ATP/AI bridge for HOL Light by combining Flyspeck’s formal mathematics with external ATPs and machine-learning premise selection. It implements the required infrastructure and evaluates automated theorem proving on the Flyspeck corpus.
- Research gap: HOL Light lacked a general bridge to large-theory ATP/AI methods that select relevant library knowledge and run external provers.The paper presents this as a natural extension of existing HOL Light work on MESON and bridges to external systems.
- Motivation: Flyspeck provides a large, interconnected corpus of formal mathematics directed toward producing a formal proof of the Kepler Conjecture.Its directed development is intended to help theorems from different areas work together when justifying new conjectures.
- Implications: The system supports semantic AI experiments over formal mathematics and enables alignment between informal and formal Flyspeck texts through corpus-driven methods.The proposed alignment uses an AI/ATP hammer as an additional semantic filter or advisor.
- Approach: The work combines sound HOL Light translations, exported proof dependencies, learned formula representations, and external advisors integrated with HOL Light.It also builds a prototype that answers mathematical queries through parallel premise selectors and ATPs.
- Evaluation: 39% of the next Flyspeck theorems were proved within 30 seconds in fully automated push-button mode on a 14-CPU workstation.Using HOL Light proof dependencies raised re-proving coverage to 50%, while the union of all evaluated methods reached 56%.
2 Translation of HOL Light Formulas to ATP formats
The paper translates HOL Light’s polymorphic higher-order logic into ATP-compatible representations while addressing type handling, higher-order application, and premise-instantiation efficiency. It contrasts the heuristic MESON translation with typed TFF1/FOF approaches and illustrates the processing on a concrete theorem.
- 2.1 Summary of the HOL Logic: HOL Light extends Church’s simple type theory with polymorphism, type operators, and higher-order features such as abstraction and currying.These features make type handling and automated reification central challenges for translation into first-order ATP formalisms.
- 2.2 The MESON Translation: The MESON translation applies β-reduction, lambda lifting, skolemization, an apply functor, and heuristic premise instantiation before invoking a first-order ATP.Its transformation is heuristic and incomplete, and is tuned for relatively small problems.
- 2.2 The MESON Translation: MESON becomes inefficient when many premises and polymorphic constants cause instantiation blow-up, so the experiments use different translations for large problems.The text also identifies incompleteness when polymorphic premises cannot be instantiated to types appearing in the goal.
- 2.3 Translation to the TFF1 and FOF Formats: Typed TFF1 and related ATP formats avoid heuristic instantiation as preprocessing by allowing ATPs to handle type-related reasoning within the generated problems.This approach uses type-aware standards such as TFF1 and THF, while FOF and SMT translations are also supported.
- 2.3 Translation to the TFF1 and FOF Formats: The TFF1 translation β-reduces formulas, removes remaining lambda abstractions through lambda lifting, and heuristically introduces an apply functor.It differs from MESON by omitting POLY_ASSUME_TAC and uses minimum application arities for higher-order constants.
- 2.3 Translation to the TFF1 and FOF Formats: The example’s original HOL Light proof uses two branches to establish equivalence between equality and equality after applying the real inverse.The surrounding discussion presents this theorem as part of the Jordan curve theorem formalization.
- 2.3 Translation to the TFF1 and FOF Formats: For re-proving, the ATP problem consists of a translated theorem together with the premises used in its original HOL Light proof.In the example, dependency tracking identifies the theorem dependencies, while only REAL_INV_INV has nontrivial first-order content after filtering.
- 2.3 Translation to the TFF1 and FOF Formats: A concrete REAL_EQ_INV example is transformed from HOL syntax into processed formulas using β-reduction, lambda lifting, and the apply functor.The exported TFF1 signature declares symbols and type operators, adds guarded quantifications, and separates overloaded constants by underlying operation.
3 Exporting Theorem Problems for Re-proving with ATPs
The paper extracts named theorem dependencies from the Flyspeck development, records proof use through a patched HOL Light kernel, and translates 14,185 proved theorems into ATP re-proving problems. It refines dependency tracking for conjunctive theorems and maintains a chronological ordering compatible with proof dependencies.
- Problem construction: The experiments use theorem-level problems rather than MESON-generated problems because MESON problems are unusually easy and may contain unsound equality merging.A manual inspection suggested that the ratio of unsound proofs was low, but theorem-level problems were considered more representative.
- Problem construction: Theorem dependencies can be collected from proofs and translated into ATP problems in systems such as Mizar/MPTP and Isabelle.The same dependency-based strategy is applied to HOL Light and Flyspeck.
- Theorem identification: HOL Light’s OCaml implementation makes theorem naming difficult because values may be unnamed, locally scoped, repeatedly generated, or inaccessible for later top-level proving.These naming issues complicate consistent dependency extraction and theorem reuse.
- Theorem identification: The update_database recording functionality inspects OCaml theorem values after loading the whole Flyspeck development to obtain a more robust theorem inventory.This records name-value pairs for theorem-typed values in a given OCaml state.
- Dependency precision: Conjunctive theorems are split into individually named conjuncts so dependency tracking records which facts a proof actually uses.This significantly prunes ATP search for theorems that previously depended on large packaged conjunctions such as ARITH.
- Theorem identification: When one theorem receives multiple names, the first name encountered during Flyspeck processing is used consistently.This method can still introduce multiple names for a single HOL Light theorem term.
- Dependency recording: A patched HOL Light kernel records newly created theorems at every inference step during a second processing of the full library.The recording component comes from HOL-Import, which was designed to transfer HOL Light proofs to Isabelle/HOL.
- Dependency normalization: Unnamed dependencies are recursively replaced by their own dependencies until every dependency of each named theorem is named.The resulting theorem order follows Flyspeck processing order and extends the partial order induced by proof dependencies.
4 Premise Selection
Premise selection combines exported theorem dependencies with learned formula features to help external ATPs prove new HOL Light conjectures without manual premise selection. The approach balances translation consistency, feature similarity, dependency quality, and online updating, while retaining limitations in representation and deployment.
- The system targets automatic proof of new theorems from a large library without manually selecting relevant premises.
- Consistent symbol naming across translations is important because inconsistent first-order symbols prevent some whole-library selection methods and model-based comparisons.The discussion contrasts optimized or multiple translations with the need for a common, consistently translated library.
- Premise-selection training uses exported HOL Light dependencies, ATP re-proving data, and iterative alternative proofs ordered chronologically.The chronological order prevents alternative proofs from introducing cycles.
- 4.1 Formula Characterizations Used for Learning: HOL formulas are characterized by normalized types, terms, atomic formulas, subterms, and nonlogical constructors for premise selection.The method adapts subterm-based characterization to typed HOL logic while filtering out logic symbols such as conjunction.
- 4.1 Formula Characterizations Used for Learning: Four variable-normalization schemes trade off broader similarity against finer distinctions based on variable identity and type.The schemes include syms0, syms, symst, and symsd; symst uses textual variable types and was used for most trainings.
- 4.1 Formula Characterizations Used for Learning: The symsd implementation produced lower performance because accidental internal type-variable numbering made most term features disjoint across theorems.It nevertheless produced unique solutions and was retained in the evaluation.
- Dynamic online premise selection can update from training data in real time, but access rights, user limits, and service cloning remain future implementation work.
5 Experiments
The experiments evaluate external ATPs and learned premise-selection methods on Flyspeck theorem-reproving tasks, using both a stable 10% subset and the full 14185-problem set. Combining complementary methods achieves substantial automated coverage, while higher time limits yield only a small gain for the final combination.
- Evaluation setup: 30-second runs use one CPU per problem on a 48-core server, with Vampire, modified E, and Z3 among the most extensively used systems.E is run through a wrapper that tries 14 strategies, rather than its standard auto-mode.
- External ATP re-proving: 50.2% of theorems are jointly re-proved when Isabelle is included, versus 47.4% with only the base systems.A parallel nine-CPU machine can prove half of the Flyspeck theorems within 30 seconds when premises are explicitly provided.
- Premise selection: 31.9% performance for ATP-only training improved the best earlier method from 29.4% and added 25 newly solved problems.The ATP-only approach was motivated by the possibility that HOL Light dependencies can guide learners toward ATP-infeasible premises.
- Premise slices: 35% is achieved in 30 seconds using 14 parallel runs of one premise-selection method, while 28 ATP runs reach the maximum 36.4% for its slice union.Only 17 of the 25 slices contribute solutions under the greedy approach.
- Final combination: 39% of all 14185 theorems are proved by the greedily selected 14-method combination in 30 seconds, while raising the time limit to 300 seconds improves the final combination by only 0.3%.The higher time limit improves the best individual method by 2.7%, but the aggregate combination gains little.
6 Initial Comparison of the Advised and Original Proofs
The comparison shows that advised ATP proofs can substantially simplify some Flyspeck theorems, although advice can also produce longer proof paths than the original HOL Light proofs. Across re-proved theorems, ATP proofs use far fewer dependencies on average.
- Overall comparison: 6162 theorems were proved by Vampire, Z3, or E from original HOL dependencies, while 5580 were proved from automatically advised premises.The two collections are compared by the number of premises used in their ATP proofs.
- Theorems proved only with advice: 885 theorems were proved only with advice; CROSS_BASIS_NONZERO required 34 premises in its advised ATP proof versus 121 HOL Light dependencies.Its HOL Light proof consists of one VEC3_TAC invocation, although that tactic introduces many dependencies.
- Examples of simpler advised proofs: FACE_OF_POLYHEDRON_POLYHEDRON received a simpler advised proof by combining face-of-still-convexity with convexity, intersection closure, and affine-hull polyhedron facts.The original 23-line HOL Light proof could not be replayed by ATPs, whereas the advised route uses three supporting facts after the structural theorem.
- Examples of simpler advised proofs: The advised proof of COMPLEX_MUL_CNJ directly uses COMPLEX_NORM_POW_2 but first unfolds complex conjugation and applies commutativity of real multiplication.The original HOL Light proof instead reuses the longer COMPLEX_NORM_POW_2 proof.
- Examples of simpler advised proofs: Advised premise selection found shorter routes by recognizing analogous results, such as affine-hull and convex-hull relationships together with negligibility preservation under inclusion.This avoided directly justifying a cardinality precondition in the convex-hull example.
- Examples of more complicated advised proofs: The advised proof of BOUNDED_CLOSURE_EQ is more complicated than the original, replacing two direct subset arguments with a longer approach through closure approximation, balls, and boundedness definitions.This illustrates that premise advice does not always recover the shortest available proof path.
7 Related Work and Contributions
The work extends large-theory AI/ATP experimentation to HOL Light and Flyspeck, combining prior approaches with new infrastructure and learning methods. Its evaluation emulates library growth by training premise selection only on earlier proofs.
- Related work: Large-theory ATP research spans automated whole-library search, user-restricted search, and benchmarks including CASC LTB and Mizar@Turing.Earlier systems include Otter-based developments, HOL and Isabelle integrations, CLAM with HOL, and Omega.
- Contributions: The system adds HOL Light and Flyspeck to the systems and corpora available for large-theory AI/ATP experiments.It reuses and adapts techniques from Mizar, Isabelle, and CASC LTB while extending them for HOL Light.
- Contributions: New HOL Light functionality supports theorem naming, dependency export, problem creation, and machine-learning advising.Feature characterization replaces variables in terms with their HOL types, and k-nearest-neighbor learning is added.
- Evaluation: The evaluation emulates library growth by training premise selection for earlier theorems without using proofs of later theorems.ATP proofs are interleaved with learning, then postprocessed by pseudo- and cross-minimization.
8 Future Work
Future work targets stronger learning, broader ATP and translation support, customizable online advising, and completed proof reconstruction. The paper also identifies possible applications to translation between informal and formal Flyspeck texts.
- Learning and representations: Stronger machine-learning methods and richer feature characterizations are expected to improve performance.Suggested additions include kernel or ensemble methods, model-evaluation features, and more abstract features.
- System extensions: The online service could learn from users’ proofs, while additional ATP systems and custom logic mappings could broaden its coverage.The current service uses three ATPs, and further translation experiments could seek symbol consistency or less incomplete translations.
- Translation and reconstruction: Future translation work includes symbol-consistent first-order translations for model-evaluation features and less incomplete translations.The paper also notes that proof reconstruction remains work in progress, with MESON over minimized dependencies as a simple proposed approach.
- Evaluation scope: A comparable large-scale evaluation for Isabelle would be interesting, although benchmark granularity may not be directly comparable.The paper notes uncertainty about whether the current Judgement Day benchmark uses theorem-level goals of the same granularity.
- Applications: The combined system could serve as a semantic aid or filter for statistical translation between informal Flyspeck text and its formalization.The paper connects this possibility to corpus-driven methods demonstrated in machine translation and natural-language query answering.