Abstract

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