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=Bba77QB2KuTideTlH6PjAmbXLO8H...

Meeting ID: 898 5609 1954 Passcode: ITPtalk