Lambda-Superposition for Successful Hammering

Add to your list(s) Download to your calendar using vCal

• Jasmin Blanchette (Ludwig-Maximilians-Universität München)
• Thursday 06 November 2025, 17:00-18:00
• Online; live-streamed at MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

Joint work with Alexander Bentkamp, Simon Cruanes, Visa Nummelin, Stephan Schulz, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann

Isabelle’s Sledgehammer, the Lean Hammer, and other hammers are useful for automatically proving theorems from mathematics and computer science. But until a few years ago, Sledgehammer relied mostly on first-order automated theorem provers, which limited its usefulness. In this talk, I will describe my work, and especially my colleagues’ work, on native higher-order provers that can serve as hammer backends. We developed lambda-superposition, a proof calculus that generalizes the highly successful superposition calculus implemented by first-order provers such as E, SPASS , and Vampire to higher-order logic. This is the logic of HOL4 , HOL Light, and Isabelle/HOL and a fragment of Lean’s logic without dependent types. The calculus is implemented in Duper, E, slam, and Zipperposition. Sledgehammer’s success rate has gone up, and Zipperposition has won trophies at system competitions.

=== Online talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• Martin's interesting talks
• Online; live-streamed at MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk449

Note that ex-directory lists are not shown.