University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Integrating Formal and Informal Reasoning

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Integrating Formal and Informal Reasoning

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Average on Sundays: 7265.84016393 kWh Department of Computer Science and technology, Lecture Theatre 2 Lecture Block, room 2, Sidgwick Site

Other talks

Director's Welcome Feedback and the circumgalactic medium Quantum optics with organic molecules Atmospheric Methane - rise, surge, and ongoing post-surge growth. Can we mitigate the rise, and can anything be done to reduce emissions? Fairy Tales Secrets of the Surface: The Mathematical Vision of Maryam Mirzakhani ( EDI Film Screening)
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity