University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Human oriented tools for theorem proving in Lean

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

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

ℹī¸ Information

Human oriented tools for theorem proving in Lean

Download to your calendar using vCal

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

I will present some tactics and tools that I made for Mathlib. I will explain how they work and show them in action with a live demonstration. The main ones are

- A library search tool for finding theorems based on an expression in the tactic state

- The generalized rewriting tactic for rewriting with relations other than equalitys.

=== Hybrid 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: 7231.94444444 kWh https://cl-cam-ac-uk.zoom.us/j/4361570789?pwd=Nkl2T3ZLaTZwRm05bzRTOUUxY3Q4QT09&from=addon TBC, possibly Pavilion C common room

Other talks

The elephant in the room: Machine Learning directly into physical models Complete and Submit Project Choice Forms Title to be confirmed Proteomics: Expression Analysis and Subcellular Localisation Polar Oceans Seminar Talk Title to be confirmed
 

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