Scientific Computing in Lean

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

• Tomas Skrivan (Carnegie Mellon University)
• Thursday 09 May 2024, 17:00-18:00
• Live-streamed at MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Jonas Bayer.

The language of science is mathematics” and Lean speaks mathematics. Since Lean 4 is an interactive theorem prover and general-purpose programming language simultaneously, it is only natural to explore its use for scientific computing.

At first glance, the advantage of using Lean is that we can fully formalize and prove the correctness of our programs. However, we will show that the utility of using an interactive theorem prover goes far beyond that. The ability to express abstract mathematical concepts allows us to build a library with an extremely high level of composability. We utilize Lean’s interactivity and tactic mode to create an interactive computer algebra system, perform source code transformations, or execute compiler optimization passes. Lean’s extensible syntax allows us to define custom domain-specific languages supporting features like probabilistic programming or write programs that are guaranteed to be differentiable.

In the past, many specialized domain-specific languages have been developed to support one of these features. Our aim is to develop a language/library where all these specialized features can coexist seamlessly.

—-

WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5

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

Note that ex-directory lists are not shown.