Integrating Formal and Informal Reasoning

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

• Chase Norman (Carnegie Mellon University)
• Thursday 04 December 2025, 17:00-18:00
• Centre for Mathematical Sciences, MR14.

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

What is the proper interface for an informal reasoner to engage in formal proof? In this talk, I will delineate a precise boundary in responsibilities between deductive procedures and informal intuition. With this, I will showcase a vision for a future-proof interface that plays to the strengths of each, without overburdening either. This allows for deep integration of machine learning methods with proof assistants, and reveals aspects of the nature of mathematics itself.

=== 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
• Centre for Mathematical Sciences, MR14
• 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
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk449

Note that ex-directory lists are not shown.