BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Jason Rute (IBM Research) DTSTART:20250115T150000Z DTEND:20250115T153000Z DTSTAMP:20261023T041633Z UID:LeanTogether2025/2 DESCRIPTION:Title: The last mile: How do we make AI theorem provers which work in th e real world for real users and not just on benchmarks?\nby Jason Rute (IBM Research) as part of Lean Together 2025\n\n\nAbstract\nAs AI researc h progresses\, we are seeing massive gains on formal math benchmarks like MiniF2F and challenges like the IMO. However\, these gains are not direct ly accessible to the typical ITP user\, nor are they used to build formal mathematical libraries. Is this because the technology is not as good as promised or because there is a disconnect between research and the day-to- day needs of users? I propose that even today\, we have sufficient AI tec hnology to enhance the experience of proof assistant users significantly. I approach this from the lens of product-focused software engineering. H ow do we bridge “the last mile” to make a useful product for the end u ser?\n LOCATION:https://researchseminars.org/talk/LeanTogether2025/2/ END:VEVENT END:VCALENDAR