NSF CAREER

Stream: general

[Tyler Josephson ⚛️]

I’m beyond excited to announce that my research group, the ATOMS Lab, got the NSF CAREER award!
We aim to use Lean to formalize theories in science and engineering (computational chemistry and thermodynamics, in particular), and write bug-free scientific computing software. To do so, we’ll teach scientists and engineers to program and prove in Lean.

[Tyler Josephson ⚛️]

Thanks to my research group, especially @Max Bobbin, @Parivash, and @Samiha Sharlin ⚛️ for putting together preliminary results for the proposal.
Also, thanks to y’all in the Lean community for making this possible, and special thanks to @Leonardo de Moura for his letter - I think this especially helped persuade the reviewers that our program had support from the Lean community.

[Tyler Josephson ⚛️]

Read more about our grant here

[Tyler Josephson ⚛️]

I should add: if you’re an undergrad, or if you know an undergrad, who wants to do a 10-week, paid REU with my lab this summer at UMBC, writing Lean proofs/code for science, send me a DM.

[Yakov Pechersky]

Regarding LeanMD, how are you planning on dealing with details of numerical stability in floating point implementations? Or is the initial attempt just assuming infinite precision?

[Tyler Josephson ⚛️]

Yakov Pechersky said:

Regarding LeanMD, how are you planning on dealing with details of numerical stability in floating point implementations? Or is the initial attempt just assuming infinite precision?

We’ll be assuming infinite precision / real numbers in our proofs and derivations - focusing on getting the high-level math and logic correct. Then, we’ll cast the final objects to floats for running computations on HPCs. We haven’t decided how - been closely watching real/float conversations here on Zulip, especially @Tomas Skrivan’s SciLean implementations. (FWIW, this paper explores your question through interval arithmetic methods)

[Alexander Bentkamp]

We've done something like that here: https://github.com/verified-optimization/CvxLean/blob/main/CvxLean/Tactic/Solver/Float/RealToFloat.lean (cc @Jeremy Avigad @Ramon Fernández Mir )

The mechanism allows us to register various expressions about the reals and their corresponding expression on floats, so that we can convert a complex real expression into an expression on floats and then evaluate it.