You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (Jul 04 2022 at 18:56):Josef Urban: Combining learning and deduction over formal math corpora
The talk will give a brief overview of recent methods that combine learning and deduction over large formal libraries. I will mention the "hammer" linkups between ITPs and ATPs, systems that learn and perform direct tactical guidance of ITPs, discuss learning of premise selection over large libraries, and learning-based guidance of saturation-style and tableau-style automated theorem provers (ATPs) trained over the large proof corpora. I will also mention feedback loops between proving and learning in this setting, and show some autoformalization and conjecturing experiments.
Zoom: https://topos-institute.zoom.us/j/84392523736?pwd=bjdVS09wZXVscjQ0QUhTdGhvZ3pUdz09
YouTube: https://www.youtube.com/watch?v=xF6OSrd8QpU