|![[Search]](https://talks.cam.ac.uk/images/search.gif?1209136071)
|![[A-Z Index]](https://talks.cam.ac.uk/images/az.gif?1209136071)
|![[Contact]](https://talks.cam.ac.uk/images/contact.gif?1209136071)
||![[University of Cambridge]](https://talks.cam.ac.uk/images/identifier2.gif?1209136071){kind=small} |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![[Talks.cam]](https://talks.cam.ac.uk/images/talkslogosmall.gif?1209136071) |
Formalisation of mathematics with interactive theorem provers
Add to your list(s)
Send you e-mail reminders
Further detail
This is a joint seminar series between the Department of Computer Science and Technology and the Faculty of Mathematics, on the fast-growing area of formalisation of mathematics with proof assistants (interactive theorem provers) such as Isabelle and Lean. All levels welcome. Undergraduate students are particularly encouraged to actively participate. Talk recordings can be found on our YouTube channel. If you have a question about this list, please contact: HoD Secretary, DPMMS; Angeliki Koutsoukou-Argyraki; Mantas Bakšys; Anand Rao Tadipatri; Jonas Bayer. If you have a question about a specific talk, click on that talk to find its organiser. 12 upcoming talks and 42 talks in the archive. How to teach Fourier analysis to a large library of formalised mathematics
Automatic Verification of BitVector Identities in SSA-Based Compiler IRs
Computer Algebra and the Formalisation of New Mathematics
Formalizing the divided power envelope in Lean
A tour in (formalised) type theory
Equational theories project: metatheorems and how to formalise them
New Foundations: the story of a large formalisation project
Computer environments for math problem solving
Reasoning with Kan fillings about Morse reductions
Alpha-Beta Pruning Explored, Extended and Verified
Little theories for big formal proofs
Teaching using a proof assistant and controlled natural language
Scientific Computing in Lean
Condensed Type Theory
Can a computer judge interestingness?(NOTE UNUSUAL DAY/TIME)
Formalising Theory of Combinatorial OptimisationOnline
Lawvere Theories in LeanOnline
Formalising (part of) the Diagonal Ramsey Paper
The Mandelbrot set is connected (and other Lean explorations)
Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry
Structures in dependent type theoryOnline
How to prove Fermat's Last TheoremOnline
Comparative Formalisation of Kneser's theorem in Isabelle/HOL and Lean
Towards Autoformalization and Mathematical Reasoning using language modelsNote unusual time
Roth numbers: Upper, lower bounds, and related constructionsNote: different room, MR20 this time
Formalizing the change of variables formula for integrals in mathlibHybrid talk (please see abstract for link) Note: different room, MR20 this time
Formalizing algebraic number theory, recent progress and future challengesNote: different room, MR20 this time
The leanest automataHybrid talk (please see abstract for link) Note: different room, MR20 this time
Formalising Erdős and Larson: Ordinal Partition Theory
Explaining mathematics using formalized mathematicsHybrid talk (please see abstract for link)
Formalization of diagram chasing as a first-order logic in CoqHybrid talk (please see abstract for link)
Smooth vector bundles in LeanHybrid talk (please see abstract for link)
Formalising modular forms, Eisenstein series and the statement of the modularity conjecture in Lean
The Locale-Centric Approach for Formalising Mathematical Hierarchies
[CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL[CANCELLED, please check back for rescheduling]
Formalising Turán's Graph Theorem in Isabelle/HOLHybrid talk (please see abstract for link)
Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
From benchmark-centric to human-centric: deep learning methods in the formalisation of mathematics
Some practical problems in formalising mathematics and how to solve themHybrid talk (please see abstract for link)
The Liquid Tensor Experiment
How Hilbert met Isabelle: Proof Between GenerationsHybrid talk (please see abstract for link)
Formalised Mathematics: Obstacles and Achievements
Please see above for contact details for this list. |
Other listsRandomised Algorithms & Processes Bus Booking Martin Centre Research Seminars, Dept of ArchitectureOther talksGateway- CCIMI Plenary Talk: Single versus double interlacing in random tiling models CANCELLED: Post Office Lives: stories of life and death in the British Post Office Measuring emissions by satellite to support the Paris Agreement Locating the Reversals: Adapting EMMA for the screen Generalised hydrodynamics of the KdV soliton gas. |
Yaël Dillies (Stockholm Universitet).
Thursday 05 December 2024, 17:00-18:00