University of Cambridge > > Formalisation of mathematics with interactive theorem provers  > Scientific Computing in Lean

Scientific Computing in Lean

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

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 : Meeting ID: 370 771 279 261 Passcode: iCo7a5

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity