Primary evidence
- HOL(y)Hammer: Online ATP Service for HOL LightS1 · Primary research · Paper · 2013-09-19
HOL(y)Hammer combines learned premise selection with ATPs for HOL Light
Users could upload HOL Light developments and ask the service to attack new conjectures using learned relevance models, parallel ATP combinations and decision procedures.
What happened?
Kaliszyk and Urban released HOL(y)Hammer as an online AI/ATP service on 19 September 2013, combining several premise-selection methods trained on project proofs with multiple automated theorem provers.
Why it matters
It provided an early mature example of machine learning embedded in a proof-assistant service over substantial formal mathematical libraries.
Significance rationale: HOL(y)Hammer deployed machine-learned premise selection and multiple automated reasoning systems as an online service for large HOL Light developments, bringing large-theory AI/ATP methods into routine formal mathematics workflows.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Substantive AI support
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- Learned models selected premises and automated provers searched for proofs, while users supplied target conjectures inside HOL Light projects.
- Human contribution
- Researchers engineered the service, learning methods, ATP portfolio, project processing and interfaces.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- holyhammer, hol-light
- Organizations
- university-of-innsbruck
- Problems
- higher-order-logic-theorem-proving
- Methods
- machine-learning, premise-selection, automated-theorem-proving, portfolio-reasoning
Sources & artifacts
- HOL(y)Hammer: Online ATP Service for HOL LightS1 · Primary research · Paper · accessed 2026-09-15
Verification history
- 2013-09-19 · Paper released · E2 · Research record
The arXiv research record establishes the service architecture and reported HOL Light deployment.
Corrections
No corrections recorded.